001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof.mgt;
012:
013: import java.util.Iterator;
014:
015: import javax.swing.tree.DefaultMutableTreeNode;
016: import javax.swing.tree.MutableTreeNode;
017:
018: import de.uka.ilkd.key.proof.Proof;
019: import de.uka.ilkd.key.proof.ProofAggregate;
020: import de.uka.ilkd.key.rule.RuleApp;
021:
022: /** Captures a node in the TaskTree which contains exactly one
023: * proof. Such a node is the only one with a one to one mapping
024: * between TaskTreeNode and Proof. It may be a sub task of a more
025: * complex task such as ProofListTask.*/
026: public class BasicTask extends DefaultMutableTreeNode implements
027: TaskTreeNode {
028:
029: private ProofAggregate proof;
030:
031: /** creates a task with a single proof. The given proof list must
032: * contain exactly one proof.*/
033: public BasicTask(ProofAggregate pl) {
034: super (pl);
035: proof = pl;
036: proof().setBasicTask(this );
037: }
038:
039: public String shortDescr() {
040: return proof().name().toString();
041: }
042:
043: public String toString() {
044: return shortDescr();
045: }
046:
047: public ProofEnvironment getProofEnv() {
048: return proof().env();
049: }
050:
051: /* returns the single proof of this task */
052: public Proof proof() {
053: return proof.getFirstProof();
054: }
055:
056: /** returns all proofs attached to this basic task*/
057: public Proof[] allProofs() {
058: return new Proof[] { proof() };
059: }
060:
061: /** inserts a node given the task tree model and a parent node */
062: public void insertNode(TaskTreeModel model,
063: MutableTreeNode parentNode) {
064: model.insertNodeInto(this , parentNode, model
065: .getChildCount(parentNode));
066: }
067:
068: /** asks the proof management component of the associated proofs
069: * for the status of the associated proof .
070: */
071: public ProofStatus getStatus() {
072: return proof().mgt().getStatus();
073: }
074:
075: /** returns a list of method contracts that were used in the
076: * associated proof.
077: */
078: public ContractSet getAllMethodContracts() {
079: Iterator it = proof().mgt().getAppliedNonAxioms();
080: ContractSet contracts = new ContractSet();
081: while (it.hasNext()) {
082: RuleApp r = (RuleApp) it.next();
083: RuleJustification rj = ((DefaultProofCorrectnessMgt) proof()
084: .mgt()).getJustification(r);
085: if (rj instanceof RuleJustificationBySpec)
086: contracts.add(((RuleJustificationBySpec) rj)
087: .getContract());
088: }
089: return contracts;
090: }
091:
092: /** returns a list of method contracts that were used in the
093: * associated proof.
094: */
095: public ContractSet getAllDLMethodContracts() {
096: Iterator it = proof().env().getSpecificationRepository()
097: .getSpecs();
098: ContractSet contracts = new ContractSet();
099: while (it.hasNext()) {
100: ContractSet c = (ContractSet) it.next();
101: contracts.addAll(c);
102: }
103: ContractSet res = new ContractSet();
104: it = contracts.iterator();
105: while (it.hasNext()) {
106: Contract c = (Contract) it.next();
107: if (c instanceof DLMethodContract)
108: res.add(c);
109: }
110: return res;
111: }
112:
113: /** returns the upper most task this basic task belongs to.*/
114: public TaskTreeNode getRootTask() {
115: TaskTreeNode tn = this ;
116: while (!(tn.getParent() instanceof EnvNode)) {
117: tn = (TaskTreeNode) tn.getParent();
118: }
119: return tn;
120: }
121:
122: /** removes the associated proof from their environment*/
123: public void decoupleFromEnv() {
124: getProofEnv().removeProofList(proof);
125: }
126:
127: }
|