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: package de.uka.ilkd.key.proof.mgt;
011:
012: import java.util.HashSet;
013: import java.util.Iterator;
014: import java.util.Set;
015:
016: import org.apache.log4j.Logger;
017:
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.proof.*;
020: import de.uka.ilkd.key.proof.init.InitConfig;
021: import de.uka.ilkd.key.proof.init.ProofOblInput;
022: import de.uka.ilkd.key.rule.*;
023:
024: /** The unique environment a proof is performed in. The environment
025: * consists of a java model, specifications, and a set of justified
026: * rules. Since the starting point of the proofs contained in the
027: * environment is equal, there is an InitConfig contained to be used
028: * to start proofs of this environment.
029: */
030: public class ProofEnvironment {
031:
032: private JavaModel jModel;
033: private RuleConfig ruleConfig;
034: private RuleJustificationInfo justifInfo = new RuleJustificationInfo();
035: private final InitConfig initConfig;
036: private Set proofs = new HashSet(); //of ProofList
037: private int number = 0;
038: private Set extraRuleSources = new HashSet(10);
039:
040: private Logger mgtLogger = Logger.getLogger("key.proof.mgt");
041:
042: /** constructs a proof environment with the given initial
043: * configuration of the proofs contained in the environment.
044: */
045: public ProofEnvironment(InitConfig initConfig) {
046: this .initConfig = initConfig;
047: }
048:
049: /** retrieves the java model underlying this environment.
050: */
051: public JavaModel getJavaModel() {
052: return jModel;
053: }
054:
055: public RuleConfig getRuleConfig() {
056: return ruleConfig;
057: }
058:
059: /** sets the java model underlying this environment. Only to be
060: * called by the {@link de.uka.ilkd.key.proof.init.ProblemInitializer}.
061: */
062: public void setJavaModel(JavaModel m) {
063: jModel = m;
064: }
065:
066: public void setRuleConfig(RuleConfig rc) {
067: ruleConfig = rc;
068: }
069:
070: public SpecificationRepository getSpecificationRepository() {
071: return getInitialServices().getSpecificationRepository();
072: }
073:
074: public Services getInitialServices() {
075: return initConfig.getServices();
076: }
077:
078: /** adds a contract to the specifications of this environment.
079: */
080: public Contract addContract(Contract ct) {
081: Contract ctResult = getSpecificationRepository().add(ct);
082: ctResult.setProofEnv(this );
083: return ctResult;
084: }
085:
086: /** adds contracts to the specifications of this environment.
087: */
088: public void addContracts(ContractSet ct, String header) {
089: Iterator it = ct.iterator();
090: while (it.hasNext()) {
091: Contract c = (Contract) it.next();
092: c.setHeader(header);
093: addContract(c);
094: }
095: }
096:
097: /** adds a method contract to the specifications of this environment
098: * and inserts the contract to the complex contract rule justification
099: */
100: public OldOperationContract addMethodContract(
101: OldOperationContract ct) {
102: OldOperationContract ctResult = (OldOperationContract) addContract(ct);
103:
104: ((ComplexRuleJustificationBySpec) getJustifInfo()
105: .getContractJustification()).add(ctResult,
106: new RuleJustificationBySpec(ctResult));
107: return ctResult;
108: }
109:
110: /** adds method contracts to the specifications of this environment
111: * and inserts the contracts to the complex contract rule justification
112: */
113: public void addMethodContracts(ContractSet ct, String header) {
114: Iterator it = ct.iterator();
115: while (it.hasNext()) {
116: Contract c = (Contract) it.next();
117: c.setHeader(header);
118: addMethodContract((OldOperationContract) c);
119: }
120: }
121:
122: /** retrieves an iterator on all specifications contained in this
123: * environment.
124: */
125: public Iterator getSpecs() {
126: return getSpecificationRepository().getSpecs();
127: }
128:
129: /** returns the object managing the rules in this environement and
130: * their justifications. The object is unique to this environment.
131: */
132: public RuleJustificationInfo getJustifInfo() {
133: return justifInfo;
134: }
135:
136: /** returns the initial configuration to be used to load proofs in
137: * this environment.
138: */
139: public InitConfig getInitConfig() {
140: return initConfig;
141: }
142:
143: /** registers a proof loaded with the given {@link
144: * de.uka.ilkd.key.proof.init.ProofOblInput}. The method adds
145: * the proof list generated by the input to the suitable contract if one
146: * is found. In all cases the proof is added to the proofs of this
147: * environment and the proofs are marked to belong to this environment.
148: */
149: public void registerProof(ProofOblInput input, ProofAggregate pl) {
150: Contractable[] contracteds = input.getObjectOfContract();
151: for (int i = 0; i < contracteds.length; i++) {
152: ContractSet cset = getSpecificationRepository()
153: .getContract(contracteds[i]);
154: if (cset != null) {
155: Iterator it = cset.iterator();
156: boolean found = false;
157: while (it.hasNext()) {
158: Contract ct = (Contract) it.next();
159: found = input.initContract(ct) || found;
160: }
161: }
162: }
163: pl.setProofEnv(this );
164: proofs.add(pl);
165: }
166:
167: /** registers a rule with the given justification at the
168: * justification managing {@link RuleJustification} object of this
169: * environment.
170: */
171: public void registerRule(Rule r, RuleJustification j) {
172: justifInfo.addJustification(r, j);
173: }
174:
175: public void registerRuleIntroducedAtNode(RuleApp r, Node node) {
176: justifInfo.addJustification(r.rule(),
177: new RuleJustificationByAddRules(node));
178: }
179:
180: public void registerRule(RuleApp r, RuleJustification j) {
181: justifInfo.addJustification(r, j);
182: }
183:
184: public void addToAllProofs(NoPosTacletApp r, RuleSource src) {
185: boolean newSource = !extraRuleSources.contains(src);
186: if (newSource)
187: extraRuleSources.add(src);
188: Iterator it = proofs.iterator();
189: while (it.hasNext()) {
190: ProofAggregate pl = (ProofAggregate) it.next();
191: Proof[] ps = pl.getProofs();
192: for (int i = 0; i < ps.length; i++) {
193: Proof p = ps[i];
194: if (newSource)
195: p.addRuleSource(src);
196: IteratorOfGoal goalIt = p.getSubtreeGoals(p.root())
197: .iterator();
198: while (goalIt.hasNext()) {
199: goalIt.next().addNoPosTacletApp(r);
200: }
201: }
202: }
203: }
204:
205: /** registers a set of rules with the given justification at the
206: * justification managing {@link RuleJustification} object of this
207: * environment. All rules of the set are given the same
208: * justification.
209: */
210: public void registerRules(SetOfTaclet s, RuleJustification j) {
211: IteratorOfTaclet it = s.iterator();
212: while (it.hasNext()) {
213: registerRule(it.next(), j);
214: }
215: }
216:
217: /** registers a list of rules with the given justification at the
218: * justification managing {@link RuleJustification} object of this
219: * environment. All rules of the list are given the same
220: * justification.
221: */
222: public void registerRules(ListOfBuiltInRule s, RuleJustification j) {
223: IteratorOfBuiltInRule it = s.iterator();
224: while (it.hasNext()) {
225: Rule r = it.next();
226: registerRule(r, j);
227: }
228: }
229:
230: /** retrieves all proofs registered at this environment
231: */
232: public Set getProofs() {
233: return proofs;
234: }
235:
236: public void removeProofList(ProofAggregate pl) {
237: proofs.remove(pl);
238: getSpecificationRepository().removeProofList(pl);
239: }
240:
241: /** returns true iff the java model equals those of the argument
242: * proof environment. TODO: extend to available rules and specs.
243: */
244: public boolean equals(Object cmp) {
245: if (!(cmp instanceof ProofEnvironment)) {
246: return false;
247: }
248: ProofEnvironment pe = (ProofEnvironment) cmp;
249: return pe.getJavaModel().equals(getJavaModel())
250: && pe.getRuleConfig().equals(getRuleConfig())
251: && pe.getNumber() == (getNumber());
252: }
253:
254: public int hashCode() {
255: int result = 5;
256: result = result * 17 + getJavaModel().hashCode();
257: result = result * 17 + getRuleConfig().hashCode();
258: result = result * 17 + getNumber();
259: return result;
260: }
261:
262: /** returns a short String description of the environment.
263: */
264: public String description() {
265: return "Env. with " + getJavaModel().description() + " #"
266: + getNumber();
267: }
268:
269: public void updateProofStatus() {
270: Set allProofs = getProofs();
271: Iterator allProofsIt = allProofs.iterator();
272: ProofAggregate pl = null;
273: while (allProofsIt.hasNext()) {
274: pl = (ProofAggregate) allProofsIt.next();
275: pl.updateProofStatus();
276: }
277: }
278:
279: public String getPureDiff(ProofEnvironment pe) {
280: CvsRunner cvs = new CvsRunner();
281: String diff = "";
282: if (!getJavaModel().isEmpty()) {
283: try {
284: diff = cvs.cvsDiff(getJavaModel().getCVSModule(), pe
285: .getJavaModel().getModelTag(), getJavaModel()
286: .getModelTag());
287: } catch (CvsException cvse) {
288: mgtLogger
289: .error("Diffing models in CVS failed: " + cvse);
290: }
291: }
292: return diff;
293: }
294:
295: public String getRuleDiff(ProofEnvironment pe) {
296: return "Rules: \n Earlier: "
297: + pe.getRuleConfig().description() + "\n Now: "
298: + getRuleConfig().description();
299: }
300:
301: public String getDiffUserInfo(ProofEnvironment pe) {
302: String base = "Comparing " + description() + " with "
303: + pe.description() + ":\n";
304: if (getJavaModel() != JavaModel.NO_MODEL
305: && !getJavaModel().getModelDir().equals(
306: pe.getJavaModel().getModelDir())) {
307: return base + "No Diff for different model directories: \n"
308: + getJavaModel().getModelDir() + " \n and "
309: + pe.getJavaModel().getModelDir();
310: }
311: return base + getPureDiff(pe) + "\n" + getRuleDiff(pe);
312: }
313:
314: /** sets a number that distinguishes two proof environments
315: * with equal java model and rule config from the user perspective
316: */
317: public void setNumber(int number) {
318: this .number = number;
319: }
320:
321: /** returns a number that distinguishes two proof environments
322: * with equal java model and rule config from the user perspective
323: */
324: public int getNumber() {
325: return number;
326: }
327:
328: public String toString() {
329: return description();
330: }
331:
332: }
|