|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.ForallTick
public class ForallTick
Implements the For All Tick rule.
Extends abstract class Rule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
ForallTick(ProofBox proof)
Constructs a ForallTick. |
Method Summary | |
---|---|
void |
addInputLine(ProofLine clickedLine)
Adds the input line to the rule. The line is checked to ensure it is a goal line. |
void |
addLine(ProofLine clickedLine)
Adds the extra lines to the rule once the input line has been added. |
void |
apply()
Called by the RuleController to apply the rule. |
void |
check()
Called by the RuleController to check the input lines to the rule. |
boolean |
checkVarSub(Formula f,
Formula f2)
Only used when the rule is applied backwards to check if the passed formula can be reached by applying For All Tick backwards on the selected line's formula. |
boolean |
haveAll()
Returns true if the rule has all of the required input lines. |
Methods inherited from class Pandora.NDRules.NDRule |
---|
checkSignature, getNewFormula |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public ForallTick(ProofBox proof)
proof
- ProofBox representing in which box the rule is being appliedMethod Detail |
---|
public void addInputLine(ProofLine clickedLine) throws java.lang.Exception
addInputLine
in class NDRule
line
- ProofLine which is the first line selected
java.lang.Exception
public void addLine(ProofLine clickedLine) throws java.lang.Exception
addLine
in class NDRule
clickedLine
- ProofLine which has been selected
java.lang.Exception
public boolean haveAll()
haveAll
in class NDRule
public void check() throws java.lang.Exception
check
in class NDRule
java.lang.Exception
public void apply() throws java.lang.Exception
apply
in class NDRule
java.lang.Exception
public boolean checkVarSub(Formula f, Formula f2) throws java.lang.Exception
java.lang.Exception
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |