| java.lang.Object
 de.uka.ilkd.key.proof.Proof
| Proof | | public class Proof implements Named(Code) | | A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals. To distinguish between open goals (the
ones we are working on) and closed goals or inner nodes we restrict
the use of the word goal to open goals which are a subset of the
proof tree's leaves. This proof class represents a proof and
encapsulates its tree structure. The
Goal class represents
a goal with all needed extra information, and methods to apply
rules. Furthermore it offers services that deliver the open goals,
namespaces and several other informations about the current state
of the proof.
|
| Field Summary | |
| public Vector | keyVersionLog
when load and save a proof with different versions of key this vector
fills up with Strings containing the prcs versions. | | public Vector | userLog
when different users load and save a proof this vector fills up with
Strings containing the user names. |
| Constructor Summary | |
| public | Proof(Services services)
| | public | Proof(String name, Services services)
| | public | Proof(String name, Term problem, String header, TacletIndex rules, BuiltInRuleIndex builtInRules, Services services, ProofSettings settings)
| | public | Proof(String name, Sequent sequent, String header, TacletIndex rules, BuiltInRuleIndex builtInRules, Services services, ProofSettings settings)
| | public | Proof(Proof p)
| | public | Proof(String name, Term problem, String header, TacletIndex rules, BuiltInRuleIndex builtInRules, Services services)
|
| keyVersionLog | | public Vector keyVersionLog(Code) | | when load and save a proof with different versions of key this vector
fills up with Strings containing the prcs versions.
|
| userLog | | public Vector userLog(Code) | | when different users load and save a proof this vector fills up with
Strings containing the user names.
|
| Proof | | public Proof(Services services)(Code) | | constructs a new empty proof
|
| add | | public void add(Goal goal)(Code) | | adds a new goal to the list of goals
Parameters:
goal - the Goal to be added |
| add | | public void add(ListOfGoal goals)(Code) | | adds a list with new goals to the list of open goals
Parameters:
goals - the ListOfGoal to be prepended |
| addProofTreeListener | | public synchronized void addProofTreeListener(ProofTreeListener listener)(Code) | | adds a listener to the proof
Parameters:
listener - the ProofTreeListener to be added |
| closeGoal | | public void closeGoal(Goal p_goal, Constraint p_c)(Code) | | Add the given constraint to the closure constraint of the given
goal, i.e. the given goal is closed if p_c is satisfied.
|
| closed | | public boolean closed()(Code) | | Return whether the remaining goals can be closed, i.e. whether
the conjunction of the constraints of the open goals is
satisfiable. In this case all remaining open goals are removed.
|
| countBranches | | public int countBranches()(Code) | | retrieves number of branches
|
| countNodes | | public int countNodes()(Code) | | retrieves number of nodes
|
| find | | public boolean find(Node node)(Code) | | returns true iff the given node is found in the proof tree
Parameters:
node - the Node to search for true iff the given node is found in the proof tree |
| fireProofClosed | | protected void fireProofClosed()(Code) | | fires the event that the proof has closed.
This event fired instead of the proofGoalRemoved event when
the last goal in list is removed.
|
| fireProofExpanded | | protected void fireProofExpanded(Node node)(Code) | | fires the event that the proof has been expanded at the given node
|
| fireProofGoalRemoved | | protected void fireProofGoalRemoved(Goal goal)(Code) | | fires the event that a goal has been removed from the list of goals
|
| fireProofGoalsAdded | | protected void fireProofGoalsAdded(ListOfGoal goals)(Code) | | fires the event that new goals have been added to the list of
goals
|
| fireProofGoalsAdded | | protected void fireProofGoalsAdded(Goal goal)(Code) | | fires the event that new goals have been added to the list of
goals
|
| fireProofGoalsChanged | | protected void fireProofGoalsChanged()(Code) | | fires the event that the proof has been restructured
|
| fireProofPruned | | protected void fireProofPruned(Node node, Node removedNode)(Code) | | fires the event that the proof has been pruned at the given node
|
| fireProofStructureChanged | | protected void fireProofStructureChanged()(Code) | | fires the event that the proof has been restructured
|
| getGoal | | public Goal getGoal(Node node)(Code) | | returns the goal that belongs to the given node or null if the
node is an inner one
the goal that belongs to the given node or null if thenode is an inner one |
| getJavaInfo | | public JavaInfo getJavaInfo()(Code) | | returns the JavaInfo with the java type information
|
| getMetavariableDeliverer | | public MetavariableDeliverer getMetavariableDeliverer()(Code) | | Deliverer of new metavariables (with unique names) |
| getNamespaces | | public NamespaceSet getNamespaces()(Code) | | returns a collection of the namespaces valid for this proof
|
| getServices | | public Services getServices()(Code) | | returns the Services with the java service classes
|
| getSubtreeGoals | | public ListOfGoal getSubtreeGoals(Node node)(Code) | | returns the list of goals of the subtree starting with node
Parameters:
node - the Node where to start from the list of goals of the subtree starting with node |
| getUserConstraint | | public ConstraintTableModel getUserConstraint()(Code) | | returns the user constraint (table model)
the user constraint |
| isGoal | | public boolean isGoal(Node node)(Code) | | returns true if the given node is part of a Goal
true if the given node is part of a Goal |
| name | | public Name name()(Code) | | returns the name of the proof. Describes in short what has to be proved.
the name of the proof |
| openGoals | | public ListOfGoal openGoals()(Code) | | returns the list of open goals
list with the open goals |
| remove | | public void remove(Goal goal)(Code) | | removes the given goal from the list of open goals. Take care
removing the last goal will fire the proofClosed event
Parameters:
goal - the Goal to be removed |
| removeClosedSubtree | | protected void removeClosedSubtree()(Code) | | Use this information to remove the goals of the closed subtree
|
| removeProofTreeListener | | public synchronized void removeProofTreeListener(ProofTreeListener listener)(Code) | | removes a listener from the proof
Parameters:
listener - the ProofTreeListener to be removed |
| replace | | public void replace(Goal oldGoal, ListOfGoal newGoals)(Code) | | removes the given goal and adds the new goals in list
Parameters:
oldGoal - the old goal that has to be removed from list
Parameters:
newGoals - the ListOfGoal with the new goals that wereresult of a rule application on goal |
| root | | public Node root()(Code) | | returns the root node of the proof
|
| setActiveStrategy | | public void setActiveStrategy(Strategy activeStrategy)(Code) | | |
| setBack | | public boolean setBack(Goal goal)(Code) | | returns true iff sets back to the step that created the given
goal. If the undo operation was succesful true is returned.
Parameters:
goal - the Goal desribing the location where to set back true iff undo operation was succesfull. |
| setBack | | public boolean setBack(Node node)(Code) | | Prunes away the subtree beneath node.
node is going to be the last node on its
branch.
Parameters:
node - the node desribing the location where to set back true iff undo operation was succesfull. |
| setNamespaces | | public void setNamespaces(NamespaceSet ns)(Code) | | sets the variable, function, sort, heuristics namespaces
|
| setRoot | | public void setRoot(Node root)(Code) | | sets the root of the proof
|
| setRuleAppIndexToAutoMode | | public void setRuleAppIndexToAutoMode()(Code) | | Currently the rule app index can either operate in interactive mode (and
contain applications of all existing taclets) or in automatic mode (and
only contain a restricted set of taclets that can possibly be applied
automated). This distinction could be replaced with a more general way to
control the contents of the rule app index
|
| setRuleAppIndexToInteractiveMode | | public void setRuleAppIndexToInteractiveMode()(Code) | | |
| setSimplifier | | public void setSimplifier(UpdateSimplifier upd_simplifier)(Code) | | sets the default simplifier
Parameters:
upd_simplifier - the UpdateSimplifier to be used asdefault (may be overwritten by branch specific simplifiers in the future) |
| simplifier | | public UpdateSimplifier simplifier()(Code) | | returns the default simplifier to be used (may be overwritten by branch
specific simplifiers in the future)
the UpdateSimplifier to be used as default one |
| subtreeCompletelyClosed | | public void subtreeCompletelyClosed(Node p_node)(Code) | | This is called by a Node that is the root of a subtree that is
closed
|
| updateProof | | public void updateProof()(Code) | | |
|
|