Pandora.NDRules
Class Reflexivity

java.lang.Object
  extended by Pandora.NDRules.NDRule
      extended by Pandora.NDRules.Reflexivity

public class Reflexivity
extends NDRule

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

Reflexivity

public Reflexivity(ProofBox proof)
Constructs a Reflexivity.

Parameters:
proof - ProofBox representing in which box the rule is being applied
Method Detail

addLine

public void addLine(ProofLine clickedLine)
             throws java.lang.Exception
Adds the extra lines to the rule once the input line has been added.

Specified by:
addLine in class NDRule
Parameters:
clickedLine - ProofLine which has been selected
Throws:
java.lang.Exception

haveAll

public boolean haveAll()
Returns true if the rule has all of the required input lines.

Specified by:
haveAll in class NDRule

check

public void check()
           throws java.lang.Exception
Called by the RuleController to check the input lines to the rule.

Specified by:
check in class NDRule
Throws:
java.lang.Exception

apply

public void apply()
           throws java.lang.Exception
Called by the RuleController to apply the rule.

Specified by:
apply in class NDRule
Throws:
java.lang.Exception

getNewTerm

protected Term getNewTerm(java.lang.String oldTerm,
                          java.lang.String message)
                   throws java.lang.Exception
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.

Parameters:
oldTerm - String represents the previous invalid Term which has been input
and will appear as the default Term on the next dialog box.
message - String represents the question message to appear on the dialog box.
Throws:
java.lang.Exception

checkSignature

public 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.

Parameters:
term - Term represents the Term which is to be checked against the signature.