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.init;
011:
012: import java.util.*;
013:
014: import recoder.io.PathList;
015: import recoder.io.ProjectSettings;
016:
017: import de.uka.ilkd.key.casetool.ModelMethod;
018: import de.uka.ilkd.key.java.*;
019: import de.uka.ilkd.key.java.abstraction.*;
020: import de.uka.ilkd.key.java.declaration.ArrayDeclaration;
021: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
022: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
023: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
024: import de.uka.ilkd.key.java.expression.operator.LessOrEquals;
025: import de.uka.ilkd.key.java.expression.operator.LessThan;
026: import de.uka.ilkd.key.java.expression.operator.New;
027: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
028: import de.uka.ilkd.key.java.reference.ArrayReference;
029: import de.uka.ilkd.key.java.reference.FieldReference;
030: import de.uka.ilkd.key.java.reference.TypeRef;
031: import de.uka.ilkd.key.java.reference.TypeReference;
032: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
033: import de.uka.ilkd.key.java.visitor.ProgramTypeCollector;
034: import de.uka.ilkd.key.jml.UsefulTools;
035: import de.uka.ilkd.key.logic.*;
036: import de.uka.ilkd.key.logic.op.*;
037: import de.uka.ilkd.key.logic.sort.ObjectSort;
038: import de.uka.ilkd.key.proof.ModifiesParserHelper;
039: import de.uka.ilkd.key.proof.OpReplacer;
040: import de.uka.ilkd.key.proof.Proof;
041: import de.uka.ilkd.key.proof.ProofAggregate;
042: import de.uka.ilkd.key.proof.RuleSource;
043: import de.uka.ilkd.key.proof.mgt.Contract;
044: import de.uka.ilkd.key.proof.mgt.Contractable;
045: import de.uka.ilkd.key.util.Debug;
046: import de.uka.ilkd.key.util.KeYExceptionHandler;
047:
048: /** represents a proof obligation originating from a given Modifies Clause
049: * as input for the prover.
050: * @deprecated Replaced by RespectsModifiesPO.
051: */
052: public class ModifiesCheckProofOblInput implements ProofOblInput {
053:
054: private ModelMethod methRepr;
055: protected String name;
056:
057: protected InitConfig initConfig;
058:
059: protected Term proofObl;
060:
061: protected SetOfTerm modifiesElements;
062: protected Set occuringClasses;
063: protected Set currentClassAttributes;
064:
065: protected KeYExceptionHandler exceptionHandler;
066:
067: protected JavaInfo javaInfo;
068: protected ProgramMethod m;
069: protected String methodName;
070:
071: protected ProgramVariable self;
072: //private ProgramVariable pv;
073: protected Vector pvVector;
074:
075: protected HashMap location2descriptor = null;
076:
077: //private Vector parameterNames = new Vector();
078: protected Vector parameterTypes;
079:
080: // private Namespace ns = new Namespace();
081:
082: private int resultNameCnt = 0;
083:
084: /** the term factory used to create terms */
085: final TermFactory tf = TermFactory.DEFAULT;
086:
087: /** creates a new representation of a proof obligation from a Modifies
088: * Clause with the given name, originating from a representation of a model
089: * method and having the given String as text of the Modifies Clause.
090: * The given XMI file name can be used to read the underlying model.
091: */
092: public ModifiesCheckProofOblInput(String name, ModelMethod aMethRepr) {
093: this .name = name
094: + (aMethRepr != null ? " " + aMethRepr.getName() : "");
095: this .methRepr = aMethRepr;
096: }
097:
098: public String getJavaPath() {
099: return methRepr.getContainingClass().getRootDirectory();
100: }
101:
102: /** returns false, that is the input never asks the user which
103: * environment he prefers
104: */
105: public boolean askUserForEnvironment() {
106: return false;
107: }
108:
109: public void setExceptionHandler(KeYExceptionHandler keh) {
110: exceptionHandler = keh;
111: }
112:
113: /** generates the proof obligation
114: *
115: */
116: public void readProblem(ModStrategy mod) {
117: if (initConfig == null) {
118: throw new IllegalStateException("InitConfig not set.");
119: }
120:
121: javaInfo = initConfig.getServices().getJavaInfo();
122:
123: getAllFromModParsHelper();
124:
125: // extracts the signature as a list
126: ListOfType signatureList = createSignatureList();
127:
128: final KeYJavaType enclosingClassType = javaInfo
129: .getKeYJavaType(methRepr.getContainingClass()
130: .getFullClassName());
131: // finds the current program method
132: m = javaInfo.getProgramMethod(enclosingClassType, methodName,
133: signatureList, enclosingClassType);
134: //last argument added. hope it is right. /AR
135:
136: // puts all occuring classes into the set occuringClasses
137: collectOccuringClasses(enclosingClassType);
138:
139: this .proofObl = createProof();
140: }
141:
142: private void getAllFromModParsHelper() {
143: ModifiesParserHelper modParserH = new ModifiesParserHelper(
144: methRepr, initConfig.getServices(), initConfig
145: .namespaces());
146:
147: // starts the internal computation of the helper class
148: modParserH.parseModifiesClauseToHashSet(methRepr
149: .getMyModifClause());
150:
151: modifiesElements = modParserH.getModifiesElements();
152: methodName = modParserH.getMethodName();
153: self = modParserH.getPVSelf();
154: pvVector = modParserH.getPVVector();
155: parameterTypes = modParserH.getParameterTypesVector();
156: }
157:
158: private ListOfType createSignatureList() {
159: ListOfType signatureList = SLListOfType.EMPTY_LIST;
160: int index = parameterTypes.size() - 1;
161: while (index >= 0) {
162: signatureList = signatureList.prepend((Type) parameterTypes
163: .elementAt(index));
164: index = index - 1;
165: }
166: return signatureList;
167: }
168:
169: protected void collectOccuringClasses(KeYJavaType type) {
170: ProgramTypeCollector mCollector = new ProgramTypeCollector(m,
171: self, type, initConfig.getServices(), new HashSet());
172: mCollector.start();
173: occuringClasses = mCollector.getResult();
174:
175: if (type != null) {
176: occuringClasses.add(type);
177: }
178:
179: // get the transitive closure of the occuring classes in the
180: // sense that for each class the type of all its' attributes
181: // is in the resulting Set
182:
183: Set occuringClassesToAdd = (HashSet) ((HashSet) occuringClasses)
184: .clone();
185: KeYJavaType current = null;
186: while (!(occuringClassesToAdd.isEmpty())) {
187: current = (KeYJavaType) occuringClassesToAdd.iterator()
188: .next();
189:
190: Type currClassType = current.getJavaType();
191: KeYJavaType currentBase = current;
192: while (currClassType instanceof ArrayDeclaration) {
193: currentBase = ((ArrayDeclaration) currClassType)
194: .getBaseType().getKeYJavaType();
195: currClassType = currentBase.getJavaType();
196: }
197: if (!(currClassType instanceof PrimitiveType || currClassType instanceof NullType)) {
198: // get all attributes of the given class
199: ListOfField allAttributes = javaInfo
200: .getKeYProgModelInfo()
201: .getAllFieldsLocallyDeclaredIn(currentBase);
202:
203: IteratorOfField iterateAttributes = allAttributes
204: .iterator();
205:
206: while (iterateAttributes.hasNext()) {
207: final ProgramVariable att = (ProgramVariable) iterateAttributes
208: .next().getProgramVariable();
209:
210: if (!att.isImplicit()) {
211: final KeYJavaType addToOccCla = (KeYJavaType) att
212: .getKeYJavaType();
213: if (!(occuringClasses.contains(addToOccCla))) {
214: occuringClasses.add(addToOccCla);
215: occuringClassesToAdd.add(addToOccCla);
216: }
217: }
218: }
219: }
220: occuringClassesToAdd.remove(current);
221: }
222: }
223:
224: protected Term createProof() {
225: Term formula;
226: if (self != null) {
227: formula = tf.createJunctorTermAndSimplify(Op.IMP, tf
228: .createJunctorTerm(Op.NOT, tf.createEqualityTerm(tf
229: .createVariableTerm(self), tf
230: .createFunctionTerm(Op.NULL))),
231: createProofStart());
232: } else {
233: formula = createProofStart();
234: }
235: return formula;
236: }
237:
238: protected Term createProofStart() {
239: Iterator iterateClasses = occuringClasses.iterator();
240: Term accumulateClassFormulas = tf.createJunctorTerm(Op.TRUE);
241: KeYJavaType currClass;
242: while (iterateClasses.hasNext()) {
243: currClass = (KeYJavaType) iterateClasses.next();
244: if (javaInfo.getNullType() != currClass) {
245: accumulateClassFormulas = tf
246: .createJunctorTermAndSimplify(Op.AND,
247: createClassFormula(currClass),
248: accumulateClassFormulas);
249: }
250: }
251: return tf.createJunctorTermAndSimplify(Op.IMP, tf
252: .createFunctionTerm(javaInfo.getInReachableState()),
253: accumulateClassFormulas);
254: }
255:
256: private Term createClassFormula(KeYJavaType currClass) {
257: LogicVariable oprime = new LogicVariable(new Name("o"),
258: currClass.getSort());
259:
260: // generate formula starting with \forall o': currClass
261: Term classFormula = tf.createQuantifierTerm(Op.ALL, oprime,
262: createClassSubFormula(currClass, oprime));
263:
264: return classFormula;
265: }
266:
267: private Term createClassSubFormula(KeYJavaType currClass,
268: LogicVariable oprime) {
269: Type currClassType = currClass.getJavaType();
270: // stop primitive types from getting checked for attributes, there are
271: // none anyway
272: if (currClassType instanceof PrimitiveType) {
273: return tf.createJunctorTerm(Op.TRUE);
274: }
275:
276: Term classSubFormula;
277:
278: ListOfField allAttributes;
279: // get all attributes of the given class
280: if (currClassType instanceof ClassDeclaration) {
281: allAttributes = javaInfo.getKeYProgModelInfo()
282: .getAllFieldsLocallyDeclaredIn(
283: javaInfo.getKeYJavaType(currClassType));
284: IteratorOfField iterateAttributes = allAttributes
285: .iterator();
286:
287: // initial value is TRUE which is the value of an empty conjunction
288: // as this formula is a conjunction this is the correct value in
289: // case there are no elements
290: Term accumulateAttributeFormulas = tf
291: .createJunctorTerm(Op.TRUE);
292:
293: ProgramVariable currAttribute = null;
294:
295: while (iterateAttributes.hasNext()) {
296: currAttribute = (ProgramVariable) iterateAttributes
297: .next().getProgramVariable();
298:
299: accumulateAttributeFormulas = tf
300: .createJunctorTermAndSimplify(Op.AND,
301: createAttributeFormula(currAttribute,
302: currClass, oprime),
303: accumulateAttributeFormulas);
304: }
305:
306: classSubFormula = accumulateAttributeFormulas;
307:
308: } else {
309: // maybe check whether it is an ArrayDeclaration with test below:
310: // check it; may be artificial nulltype
311: if (currClassType instanceof ArrayDeclaration) {
312: classSubFormula = createArrayFormula(currClass, oprime);
313: } else {
314: // is this correct?
315: classSubFormula = tf.createJunctorTerm(Op.TRUE);
316: }
317: }
318:
319: Term nullTerm = tf.createFunctionTerm(Op.NULL);
320: Term ov = tf.createVariableTerm(oprime);
321: Term nn = tf.createJunctorTerm(Op.NOT, tf.createEqualityTerm(
322: ov, nullTerm));
323:
324: Term eqc = UsefulTools.isCreated(ov, initConfig.getServices());
325: ProgramVariable ci = initConfig.getServices().getJavaInfo()
326: .getAttribute(
327: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
328: (ObjectSort) oprime.sort());
329:
330: Term eqi = tf.createEqualityTerm(tf.createVariableTerm(ci),
331: initConfig.getServices().getTypeConverter()
332: .convertToLogicElement(BooleanLiteral.TRUE));
333: eqc = tf.createJunctorTermAndSimplify(Op.AND, eqc, eqi);
334: classSubFormula = tf.createJunctorTermAndSimplify(Op.IMP, tf
335: .createJunctorTerm(Op.AND, nn, eqc), classSubFormula);
336: return classSubFormula;
337: }
338:
339: private Term createAttributeFormula(ProgramVariable currAttribute,
340: KeYJavaType currClass, LogicVariable oprime) {
341: if (!currAttribute.isImplicit()) {
342:
343: // create conjunction of o' != o111, o' != o112, ... for non-static
344: // create "false" in case of a static attribute which is part of
345: // the modifies clause and "true" if it not part of the m.c.
346:
347: // some initial value
348: Term ante = tf.createJunctorTerm(Op.TRUE);
349:
350: IteratorOfTerm modifiesIterator = modifiesElements
351: .iterator();
352: TypeConverter typeConv = initConfig.getServices()
353: .getTypeConverter();
354: final Term t_oprime = tf.createVariableTerm(oprime);
355:
356: while (modifiesIterator.hasNext()) {
357: Term modTerm = modifiesIterator.next();
358:
359: if ((!(modTerm.op() instanceof ProgramVariable) || ((ProgramVariable) modTerm
360: .op()).isStatic())
361: && !(modTerm.op() instanceof ArrayOp)) {
362: ante = createModifiesFormulaForAttribute(
363: currAttribute, currClass, ante, modTerm,
364: typeConv, t_oprime);
365: } else {
366: if (modTerm.op() instanceof ProgramVariable) {
367: // The modifies element has been a single ProgramVariable,
368: // meaning no dereferencing has happened. In this case there
369: // is nothing that can be done because this shouldn't happen
370: // Only attributes can be changed and thus only those are
371: // relevant in the modifies clause.
372: // THROW EXCEPTION HERE !!!
373: System.out
374: .println("Error - Element with no dereferencing "
375: + "in the modifies clause: "
376: + modTerm);
377: }
378: if (modTerm.op() instanceof ArrayOp) {
379: // nothing to do here as an array element is not
380: // relevant for a normal attribute
381: }
382: }
383: }
384:
385: // create part after the implication arrow
386: LogicVariable x = new LogicVariable(new Name("x"),
387: currAttribute.getKeYJavaType().getSort());
388:
389: // Create the MethodReference belonging to the method whose modifies
390: // clause is being checked here.
391: Expression[] p = new Expression[pvVector.size()];
392: for (int i = 0; i < pvVector.size(); i = i + 1) {
393: p[i] = (ProgramVariable) pvVector.elementAt(i);
394: }
395:
396: StatementBlock mBlock = createMethodCall(p);
397:
398: final Term t_x = tf.createVariableTerm(x);
399: final Term primedAttribute = tf.createAttributeTerm(
400: currAttribute, t_oprime);
401:
402: Term post = tf.createQuantifierTerm(Op.ALL, x, tf
403: .createJunctorTermAndSimplify(Op.IMP, tf
404: .createEqualityTerm(t_x, primedAttribute),
405: tf.createBoxTerm(JavaBlock
406: .createJavaBlock(mBlock), tf
407: .createEqualityTerm(t_x,
408: primedAttribute))));
409:
410: return tf.createJunctorTermAndSimplify(Op.IMP, ante, post);
411: } else {
412: return tf.createJunctorTerm(Op.TRUE);
413: }
414: }
415:
416: /**
417: * @param currAttribute
418: * @param currClass
419: * @param ante
420: * @param modProgVar
421: * @param typeConv
422: * @param t_oprime
423: * @return
424: */
425: private Term createModifiesFormulaForAttribute(
426: ProgramVariable currAttribute, KeYJavaType currClass,
427: Term ante, Term modTerm, TypeConverter typeConv,
428: final Term t_oprime) {
429:
430: // static attribute
431: if (modTerm.op() instanceof ProgramVariable) {
432: // Check if the attributes match
433: if (modTerm.op() == currAttribute) {
434: // build formula
435: ante = tf.createJunctorTerm(Op.FALSE);
436: }
437: } else {
438: ProgramVariable modProgAttrib = (ProgramVariable) ((AttributeOp) modTerm
439: .op()).attribute();
440: BasicLocationDescriptor bloc = (BasicLocationDescriptor) location2descriptor
441: .get(modTerm);
442: modTerm = modTerm.sub(0);
443:
444: KeYJavaType classType = javaInfo.getKeYJavaType(modTerm
445: .sort());
446: // Check if the Class Types match
447: if (classType == currClass) {
448: // Check if the attributes match
449: if (modProgAttrib == currAttribute) {
450: Term anteSub = tf.createJunctorTerm(Op.NOT, tf
451: .createEqualityTerm(t_oprime, modTerm));
452: anteSub = tf.createJunctorTermAndSimplify(Op.IMP,
453: bloc.getFormula(), anteSub);
454: // quantify free variables in the prefix
455: if (modTerm.freeVars().size() > 0) {
456: anteSub = tf
457: .createQuantifierTerm(
458: Op.ALL,
459: new ArrayOfQuantifiableVariable(
460: modTerm.freeVars()
461: .toArray()),
462: anteSub);
463: }
464: // build formula
465: ante = tf.createJunctorTermAndSimplify(Op.AND,
466: anteSub, ante);
467: }
468: }
469: }
470: return ante;
471:
472: }
473:
474: private Term createArrayFormula(KeYJavaType currClass,
475: LogicVariable oprime) {
476: // create conjunction of o' != o111, o' != o112, ...
477: // all this with a "check" before it for the right array index
478:
479: TypeConverter typeConv = initConfig.getServices()
480: .getTypeConverter();
481:
482: LogicVariable lambda = new LogicVariable(new Name("lambda"),
483: typeConv.getIntegerLDT().targetSort());
484:
485: // initial value true, as it is the value of an empty conjunction
486: // and our terms are connected conjunctively
487: Term ante = tf.createJunctorTerm(Op.TRUE);
488:
489: IteratorOfTerm modifiesIterator = modifiesElements.iterator();
490: while (modifiesIterator.hasNext()) {
491: Term modTerm = modifiesIterator.next();
492: // modElm = typeConv.convertToProgramElement(modTerm);
493:
494: // modProgVar = modElm;
495:
496: //check whether it is appropriate to add this to the ante
497: // if (modProgVar instanceof ArrayReference){
498: if (modTerm.op() instanceof ArrayOp
499: && javaInfo.getKeYJavaType(modTerm.sub(0).sort()) == currClass) {
500: Term preCond = tf.createJunctorTerm(Op.TRUE);
501: if (modTerm.sub(1).freeVars().size() == 0) {
502: preCond = tf.createEqualityTerm(modTerm.sub(1), tf
503: .createVariableTerm(lambda));
504: }
505: Debug.assertTrue(modTerm.sub(1).freeVars().size() <= 1);
506: BasicLocationDescriptor bloc = (BasicLocationDescriptor) location2descriptor
507: .get(modTerm);
508: HashMap replaceMap = new HashMap();
509: replaceMap.put(modTerm.sub(1).freeVars().iterator()
510: .next(), lambda);
511: OpReplacer or = new OpReplacer(replaceMap);
512: preCond = tf.createJunctorTermAndSimplify(Op.AND,
513: preCond, or.replace(bloc.getFormula()));
514: // o' != o_ij
515: Term postCond = tf.createJunctorTerm(Op.NOT, tf
516: .createEqualityTerm(tf
517: .createVariableTerm(oprime), modTerm
518: .sub(0)));
519:
520: Term cond = tf.createJunctorTermAndSimplify(Op.IMP,
521: preCond, postCond);
522:
523: // quantify free variables in the prefix
524: if (modTerm.sub(0).freeVars().size() > 0) {
525: cond = tf
526: .createQuantifierTerm(Op.ALL,
527: new ArrayOfQuantifiableVariable(
528: modTerm.sub(0).freeVars()
529: .toArray()), cond);
530: }
531:
532: // build parts together into the ante formula
533: ante = tf.createJunctorTermAndSimplify(Op.AND, cond,
534: ante);
535: } else {
536: // The modifies element has not been an ArrayReference,
537: // that means it has nothing to do with the current class/array
538: // as that is an array and we can thus ignore this element of
539: // the modifies clause
540: }
541: }
542:
543: // create part after the outer implication arrow
544: LogicVariable x = new LogicVariable(new Name("x"),
545: ((ArrayDeclaration) currClass.getJavaType())
546: .getBaseType().getKeYJavaType().getSort());
547:
548: // Create the MethodReference belonging to the method whose modifies
549: // clause is being checked here.
550: Expression[] p = new Expression[pvVector.size()];
551: for (int i = 0; i < pvVector.size(); i = i + 1) {
552: p[i] = (ProgramVariable) pvVector.elementAt(i);
553: }
554:
555: StatementBlock mBlock = createMethodCall(p);
556:
557: Term equality = tf.createEqualityTerm(tf.createVariableTerm(x),
558: tf.createArrayTerm(ArrayOp.getArrayOp(oprime.sort()),
559: tf.createVariableTerm(oprime), tf
560: .createVariableTerm(lambda)));
561:
562: Term post = tf.createQuantifierTerm(Op.ALL, x, tf
563: .createJunctorTermAndSimplify(Op.IMP, equality, tf
564: .createBoxTerm(JavaBlock
565: .createJavaBlock(mBlock), equality)));
566:
567: Term arrayFormula = tf.createJunctorTermAndSimplify(Op.IMP,
568: ante, post);
569:
570: // helpers for the next block below
571: final Function leq = typeConv.getIntegerLDT().getLessOrEquals();
572: final Function lt = typeConv.getIntegerLDT().getLessThan();
573: final Term zero = typeConv.getIntegerLDT().translateLiteral(
574: new IntLiteral(0));
575: final Term validArrayTerm0 = tf.createFunctionTerm(leq, zero,
576: tf.createVariableTerm(lambda));
577: final ProgramVariable lengthPV = (ProgramVariable) ((ArrayDeclaration) currClass
578: .getJavaType()).length().getFieldSpecifications()
579: .getFieldSpecification(0).getProgramVariable();
580: final Term lengthTerm = tf.createAttributeTerm(lengthPV, tf
581: .createVariableTerm(oprime));
582: final Term validArrayTerm1 = tf.createFunctionTerm(lt, tf
583: .createVariableTerm(lambda), lengthTerm);
584:
585: // creates the 0<= lambda /\ lambda < o'.length() -> rest
586: arrayFormula = tf.createJunctorTermAndSimplify(Op.IMP, tf
587: .createJunctorTermAndSimplify(Op.AND, validArrayTerm0,
588: validArrayTerm1), arrayFormula);
589:
590: // generate and return formula starting with \forall \lambda: int
591: return tf.createQuantifierTerm(Op.ALL, lambda, arrayFormula);
592: }
593:
594: private StatementBlock createMethodCall(Expression[] p) {
595: if (m.isConstructor()) {
596: TypeRef prefix = new TypeRef(self.getKeYJavaType());
597: New n = new New(p, prefix, prefix);
598: return new StatementBlock(n);
599: } else {
600: ProgramVariable result = null;
601: if (m.getKeYJavaType() != null) {
602: result = new LocationVariable(new ProgramElementName(
603: "_result" + resultNameCnt++), m
604: .getKeYJavaType());
605: initConfig.namespaces().programVariables().add(result);
606: }
607: MethodBodyStatement mBS = new MethodBodyStatement(m, self,
608: result, new ArrayOfExpression(p));
609: return new StatementBlock(mBS);
610: }
611: }
612:
613: public ProofAggregate getPO() {
614: if (proofObl == null)
615: throw new IllegalStateException("No proofObl term");
616: // now a static call since there is no suitable common superclass
617: String s = OCLProofOblInput.createProofHeader(initConfig,
618: methRepr.getContainingClass().getRootDirectory());
619: return ProofAggregate.createProofAggregate(new Proof(name(),
620: proofObl, s, initConfig.createTacletIndex(), initConfig
621: .createBuiltInRuleIndex(), initConfig
622: .getServices()), name());
623: }
624:
625: /** sets the initial configuration that is used to read the OCL
626: * input and that is used to be modified during reading.
627: */
628: public void setInitConfig(InitConfig conf) {
629: this .initConfig = conf;
630: initConfig.sortNS().startProtocol();
631: initConfig.funcNS().startProtocol();
632: initConfig.progVarNS().startProtocol();
633: }
634:
635: /** returns the name of the modifies check proof obligation input.
636: */
637: public String name() {
638: return name;
639: }
640:
641: public void readActivatedChoices() throws ProofInputException {
642:
643: }
644:
645: /** reads the include section and returns an Includes object.
646: */
647: public Includes readIncludes() throws ProofInputException {
648: RuleSource standard = RuleSource
649: .initRuleFile("standardRules.key");
650: Includes includes = new Includes();
651: includes.put("standardRules", standard);
652: return includes;
653: }
654:
655: public void readSpecs() {
656: // nothing here
657: }
658:
659: public Term getPOTerm() {
660: return proofObl;
661: }
662:
663: public SetOfTerm getModifiesElements() {
664: return modifiesElements;
665: }
666:
667: public Contractable[] getObjectOfContract() {
668: return new Contractable[] { methRepr };
669: }
670:
671: public boolean initContract(Contract ct) {
672: return false; //%%
673: }
674:
675: public void startProtocol() {
676: // do nothing
677: }
678:
679: }
|