|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.Reflexivity
public class Reflexivity
Implements the Reflexivity rule.
Extends abstract class NDRule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
Reflexivity(ProofBox proof)
Constructs a Reflexivity. |
Method Summary | |
---|---|
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 |
checkSignature(Term term)
Returns false if the passed Term clashes with or is not included in the signature of the box this rule is applied in, true otherwise. |
protected Term |
getNewTerm(java.lang.String oldTerm,
java.lang.String message)
This method is used only when Reflexivity rule is applied forwards, to get a term to substitute the left and right hand side of the newly introduced Equals Formula. The returned Term must be in the signature of the box in which this rule is applied in. |
boolean |
haveAll()
Returns true if the rule has all of the required input lines. |
Methods inherited from class Pandora.NDRules.NDRule |
---|
addInputLine, checkSignature, getNewFormula |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public Reflexivity(ProofBox proof)
proof
- ProofBox representing in which box the rule is being appliedMethod Detail |
---|
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
protected Term getNewTerm(java.lang.String oldTerm, java.lang.String message) throws java.lang.Exception
oldTerm
- String represents the previous invalid Term which has been inputmessage
- String represents the question message to appear on the dialog box.
java.lang.Exception
public boolean checkSignature(Term term)
term
- Term represents the Term which is to be checked against the signature.
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |