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.casetool;
012:
013: import java.io.File;
014: import java.util.*;
015:
016: import de.uka.ilkd.key.casetool.together.TogetherEnvInput;
017: import de.uka.ilkd.key.casetool.together.TogetherModelClass;
018: import de.uka.ilkd.key.gui.ClassInvariantSelectionDialog;
019: import de.uka.ilkd.key.gui.ClassSelectionDialog;
020: import de.uka.ilkd.key.gui.Main;
021: import de.uka.ilkd.key.gui.SuperclassSelectionDialog;
022: import de.uka.ilkd.key.java.JavaInfo;
023: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
024: import de.uka.ilkd.key.logic.ProgramElementName;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.proof.init.*;
027: import de.uka.ilkd.key.speclang.*;
028: import de.uka.ilkd.key.util.Debug;
029:
030: public class FunctionalityOnModel {
031:
032: private static final InvariantSelectionStrategy invStrategy = InvariantSelectionStrategy.PRESELECT_CLASS;
033:
034: private FunctionalityOnModel() {
035: }
036:
037: private static String startProver(ModelClass modelClass,
038: ProofOblInput po) {
039: ProblemInitializer pi = new ProblemInitializer(Main
040: .getInstance());
041: EnvInput envInput = new TogetherEnvInput(
042: (TogetherModelClass) modelClass);
043: try {
044: pi.startProver(envInput, po);
045: } catch (ProofInputException e) {
046: return e.toString();
047: }
048: return "";
049: }
050:
051: /**
052: * Returns the method overridden by subMethod in the passed supertype,
053: * or null if no such method exists.
054: */
055: private static ModelMethod getOverriddenMethod(
056: ModelMethod subMethod, ModelClass super type) {
057: Vector v = super type.getOps();
058: Iterator it = v.iterator();
059: String name = subMethod.getName();
060: int numParameters = subMethod.getNumParameters();
061: ModelMethod overriddenMethod = null;
062: while (it.hasNext()) {
063: ModelMethod super Method = (ModelMethod) (it.next());
064: if (name.equals(super Method.getName())
065: && numParameters == super Method.getNumParameters()) {
066: boolean parametersEqual = true;
067:
068: for (int i = 0; i < numParameters; i++) {
069: if (!subMethod.getParameterTypeAt(i).equals(
070: super Method.getParameterTypeAt(i))) {
071: parametersEqual = false;
072: break;
073: }
074: }
075:
076: if (parametersEqual) {
077: overriddenMethod = super Method;
078: break;
079: }
080: }
081: }
082:
083: return overriddenMethod;
084: }
085:
086: protected static LogicVariable buildSelfVarAsLogicVar(
087: ModelClass modelClass, JavaInfo javaInfo) {
088: String className = modelClass.getFullClassName();
089: KeYJavaType classType = javaInfo.getTypeByClassName(className);
090:
091: ProgramElementName classPEN = new ProgramElementName("self");
092: LogicVariable result = new LogicVariable(classPEN, classType
093: .getSort());
094:
095: return result;
096: }
097:
098: protected static ListOfParsableVariable buildParamVars(
099: ModelMethod modelMethod, JavaInfo javaInfo) {
100: int numPars = modelMethod.getNumParameters();
101: ListOfParsableVariable result = SLListOfParsableVariable.EMPTY_LIST;
102:
103: for (int i = 0; i < numPars; i++) {
104: KeYJavaType parType = javaInfo
105: .getTypeByClassName(modelMethod
106: .getParameterTypeAt(i));
107: assert parType != null;
108: ProgramElementName parPEN = new ProgramElementName(
109: modelMethod.getParameterNameAt(i));
110: result = result
111: .append(new LocationVariable(parPEN, parType));
112: }
113:
114: return result;
115: }
116:
117: protected static ProgramVariable buildResultVar(
118: ModelMethod modelMethod, JavaInfo javaInfo) {
119: ProgramVariable result = null;
120:
121: if (!modelMethod.isVoid()) {
122: KeYJavaType resultType = javaInfo
123: .getTypeByClassName(modelMethod.getResultType());
124: assert resultType != null;
125: ProgramElementName resultPEN = new ProgramElementName(
126: "result");
127: result = new LocationVariable(resultPEN, resultType);
128: }
129:
130: return result;
131: }
132:
133: protected static ProgramVariable buildExcVar(JavaInfo javaInfo) {
134: KeYJavaType excType = javaInfo
135: .getTypeByClassName("java.lang.Throwable");
136: ProgramElementName excPEN = new ProgramElementName("exc");
137: ProgramVariable result = new LocationVariable(excPEN, excType);
138:
139: return result;
140: }
141:
142: /**
143: * parse the invariant of a class if available.
144: * @param aReprModelClass the class whose invariant should be parsed
145: * @return error message to the user
146: */
147: public static String parseOneInvariant(UMLModelClass aReprModelClass) {
148: String result = "";
149:
150: ListOfClassInvariant invs = aReprModelClass
151: .getMyClassInvariants();
152: if (invs.isEmpty()) {
153: result = "No invariant available";
154: } else {
155:
156: ProblemInitializer pi = new ProblemInitializer(Main
157: .getInstance());
158: EnvInput envInput = new TogetherEnvInput(
159: (TogetherModelClass) aReprModelClass);
160:
161: InitConfig initConf = null;
162:
163: try {
164: initConf = pi.prepare(envInput);
165: } catch (ProofInputException e) {
166: e.printStackTrace();
167: Debug.fail("initialising proover failed.");
168: }
169:
170: assert initConf != null;
171:
172: IteratorOfClassInvariant invIterator = invs.iterator();
173:
174: while (invIterator.hasNext()) {
175: try {
176: invIterator.next().getInv(initConf.getServices());
177: } catch (SLTranslationError e) {
178: result += "Error in Invariant:\n" + e.getLine()
179: + ":" + e.getColumn() + " "
180: + e.getMessage() + "\n\n";
181: }
182:
183: if (initConf.getServices().getExceptionHandler()
184: .error()) {
185: Iterator errors = initConf.getServices()
186: .getExceptionHandler().getExceptions()
187: .iterator();
188: while (errors.hasNext()) {
189: Exception e = (Exception) errors.next();
190: if (e instanceof antlr.RecognitionException) {
191: result += "Error in Invariant:\n"
192: + ((antlr.RecognitionException) e)
193: .getLine()
194: + ":"
195: + ((antlr.RecognitionException) e)
196: .getColumn()
197: + " "
198: + ((antlr.RecognitionException) e)
199: .getMessage() + "\n\n";
200: }
201: }
202: }
203: }
204:
205: }
206:
207: return result.equals("") ? "No Errors were found." : result;
208: }
209:
210: /**
211: * parse the throughout property of a class if available.
212: * @param aReprModelClass the class whose throughout should be parsed
213: * @return error message to the user
214: */
215: public static String parseOneThroughout(
216: UMLModelClass aReprModelClass) {
217: String result = "";
218:
219: ListOfClassInvariant invs = aReprModelClass
220: .getMyThroughoutClassInvariants();
221: if (invs.isEmpty()) {
222: result = "No invariant available";
223: } else {
224:
225: ProblemInitializer pi = new ProblemInitializer(Main
226: .getInstance());
227: EnvInput envInput = new TogetherEnvInput(
228: (TogetherModelClass) aReprModelClass);
229:
230: InitConfig initConf = null;
231:
232: try {
233: initConf = pi.prepare(envInput);
234: } catch (ProofInputException e) {
235: e.printStackTrace();
236: Debug.fail("initialising proover failed.");
237: }
238:
239: assert initConf != null;
240:
241: IteratorOfClassInvariant invIterator = invs.iterator();
242:
243: while (invIterator.hasNext()) {
244: try {
245: invIterator.next().getInv(initConf.getServices());
246: } catch (SLTranslationError e) {
247: result += "Error in Invariant:\n" + e.getLine()
248: + ":" + e.getColumn() + " "
249: + e.getMessage() + "\n\n";
250: }
251:
252: if (initConf.getServices().getExceptionHandler()
253: .error()) {
254: Iterator errors = initConf.getServices()
255: .getExceptionHandler().getExceptions()
256: .iterator();
257: while (errors.hasNext()) {
258: Exception e = (Exception) errors.next();
259: if (e instanceof antlr.RecognitionException) {
260: result += "Error in Invariant:\n"
261: + ((antlr.RecognitionException) e)
262: .getLine()
263: + ":"
264: + ((antlr.RecognitionException) e)
265: .getColumn()
266: + " "
267: + ((antlr.RecognitionException) e)
268: .getMessage() + "\n\n";
269: }
270: }
271: }
272: }
273:
274: }
275:
276: return result.equals("") ? "No Errors were found." : result;
277: }
278:
279: /**
280: * Starts the prover with an "EnsuresPost" proof obligation.
281: * @param modelMethod the ModelMethod to reason about; the proof obligation
282: * will be about its *first* OperationContract
283: * @return error message to the user
284: */
285: public static String parseMethodSpec(ModelMethod modelMethod) {
286: //get the relevant contract
287: ListOfOperationContract contracts = modelMethod
288: .getMyOperationContracts();
289: if (contracts.isEmpty()) {
290: return "No contracts are available for the selected method.";
291: }
292: OperationContract contract = contracts.head();
293:
294: String result = "";
295:
296: ProblemInitializer pi = new ProblemInitializer(Main
297: .getInstance());
298: EnvInput envInput = new TogetherEnvInput(
299: (TogetherModelClass) modelMethod.getContainingClass());
300:
301: InitConfig initConf = null;
302:
303: try {
304: initConf = pi.prepare(envInput);
305: } catch (ProofInputException e) {
306: e.printStackTrace();
307: Debug.fail("initialising proover failed.");
308: }
309:
310: assert initConf != null;
311:
312: ParsableVariable selfVar = buildSelfVarAsLogicVar(modelMethod
313: .getContainingClass(), initConf.getServices()
314: .getJavaInfo());
315:
316: ListOfParsableVariable paramVars = buildParamVars(modelMethod,
317: initConf.getServices().getJavaInfo());
318:
319: ParsableVariable resultVar = buildResultVar(modelMethod,
320: initConf.getServices().getJavaInfo());
321:
322: ParsableVariable excVar = buildExcVar(initConf.getServices()
323: .getJavaInfo());
324:
325: try {
326: contract.getPre(selfVar, paramVars, initConf.getServices());
327: } catch (SLTranslationError e) {
328: result += "Error in Pre Condition:\n" + e.getLine() + ":"
329: + e.getColumn() + " " + e.getMessage() + "\n\n";
330: }
331:
332: if (initConf.getServices().getExceptionHandler().error()) {
333: Iterator errors = initConf.getServices()
334: .getExceptionHandler().getExceptions().iterator();
335: while (errors.hasNext()) {
336: Exception e = (Exception) errors.next();
337: if (e instanceof antlr.RecognitionException) {
338: result += "Error in Pre Condition:\n"
339: + ((antlr.RecognitionException) e)
340: .getLine()
341: + ":"
342: + ((antlr.RecognitionException) e)
343: .getColumn()
344: + " "
345: + ((antlr.RecognitionException) e)
346: .getMessage() + "\n\n";
347: }
348: }
349: }
350:
351: try {
352: contract.getPost(selfVar, paramVars, resultVar, excVar,
353: initConf.getServices());
354: } catch (SLTranslationError e) {
355: result += "Error in Post Condition:\n" + e.getLine() + ":"
356: + e.getColumn() + " " + e.getMessage() + "\n";
357: }
358:
359: if (initConf.getServices().getExceptionHandler().error()) {
360: Iterator errors = initConf.getServices()
361: .getExceptionHandler().getExceptions().iterator();
362: while (errors.hasNext()) {
363: Exception e = (Exception) errors.next();
364: if (e instanceof antlr.RecognitionException) {
365: result += "Error in Post Condition:\n"
366: + ((antlr.RecognitionException) e)
367: .getLine()
368: + ":"
369: + ((antlr.RecognitionException) e)
370: .getColumn()
371: + " "
372: + ((antlr.RecognitionException) e)
373: .getMessage() + "\n\n";
374: }
375: }
376: }
377:
378: return result.equals("") ? "No Errors were found." : result;
379: }
380:
381: /**
382: * Computes and displays the specification of the method.
383: * Tries to compute the strongest specification (pre and postcondition)
384: * of <code>aMethRepr</code>.
385: * @param modelMethod the method whose specification to compute.
386: * @return any error messages to pass to the user.
387: * @see de.uka.ilkd.key.cspec.ComputeSpecification
388: * @see de.uka.ilkd.key.proof.init.ComputeSpecificationPONew
389: */
390: public static String computeSpecification(ModelMethod modelMethod) {
391:
392: ProofOblInput po = new ComputeSpecificationPONew(
393: "ComputeSpecification", modelMethod);
394:
395: return startProver(modelMethod.getContainingClass(), po);
396: }
397:
398: public static String transformXMIFile(ReprModel aReprModel) {
399: return "";
400: }
401:
402: public static String proveDLFormula(ModelClass modelClass, File file) {
403:
404: CasetoolDLPO dlPOFromCasetool = new CasetoolDLPO(modelClass,
405: file);
406: return startProver(modelClass, dlPOFromCasetool);
407: }
408:
409: /**
410: * Used for OCL Simplification.
411: * @param modelClass the ModelClass whose invariant needs to be simplified.
412: */
413: public static String simplifyInvariant(ModelClass modelClass) {
414: ProofOblInput po = new OCLInvSimplPO(modelClass);
415: return startProver(modelClass, po);
416: }
417:
418: //-------------------------------------------------------------------------
419: //New proof obligations
420: //-------------------------------------------------------------------------
421:
422: /**
423: * Asks the user to choose a supertype and then starts the prover with a
424: * corresponding "BehaviouralSubtypingInv" proof obligation.
425: * @param subtype the UMLModelClass with subtype for which behavioural
426: * subtyping with respect to the invariant has to be shown
427: * @return error message to the user
428: */
429: public static String proveBehaviouralSubtypingInv(
430: UMLModelClass subtype) {
431: //let the user select a supertype
432: SuperclassSelectionDialog dlg = new SuperclassSelectionDialog(
433: subtype);
434: if (!dlg.wasSuccessful()) {
435: return "";
436: }
437: ModelClass super type = dlg.getSuperclass();
438: if (super type == null) {
439: return "No supertype has been selected.";
440: }
441: if (super type.getMyClassInvariants().isEmpty()) {
442: return "Supertype does not have any invariants.";
443: }
444:
445: //create and start the PO
446: final ProofOblInput po = new BehaviouralSubtypingInvPO(subtype,
447: super type);
448: return startProver(subtype, po);
449: }
450:
451: /**
452: * Starts the prover with a "BehaviouralSubtypingOpPair" proof obligation.
453: * @param subMethod the ModelMethod representing the overwriting method to reason about; the proof
454: * obligation will be about its *first* operation contract
455: * @return error message to the user
456: */
457: public static String proveBehaviouralSubtypingOpPair(
458: ModelMethod subMethod) {
459: //get the relevant contract of the subtype method
460: ListOfOperationContract subContracts = subMethod
461: .getMyOperationContracts();
462: if (subContracts.isEmpty()) {
463: return "No contracts are available for the selected method.";
464: }
465: OperationContract subContract = subContracts.head();
466:
467: //let the user select a supertype
468: //(eventually, the user should be allowed to choose a specific contract
469: //here instead of just a class)
470: SuperclassSelectionDialog dlg = new SuperclassSelectionDialog(
471: subMethod.getContainingClass());
472: if (!dlg.wasSuccessful()) {
473: return "";
474: }
475: ModelClass super type = dlg.getSuperclass();
476: if (super type == null) {
477: return "No supertype has been selected";
478: }
479:
480: //determine the method in the chosen supertype which is overriden
481: //by the subtype method
482: ModelMethod overriddenMethod = getOverriddenMethod(subMethod,
483: super type);
484: if (overriddenMethod == null) {
485: return "No overridden method \"" + subMethod.getName()
486: + "\" could be found in the selected supertype.";
487: }
488:
489: //get the relevant contract of the overridden method
490: ListOfOperationContract overriddenContracts = overriddenMethod
491: .getMyOperationContracts();
492: if (overriddenContracts.isEmpty()) {
493: return "No contracts are available for the overridden method.";
494: }
495: OperationContract overriddenContract = overriddenContracts
496: .head();
497:
498: //create and start the PO
499: ProofOblInput po = new BehaviouralSubtypingOpPairPO(
500: subContract, overriddenContract);
501: return startProver(super type, po);
502: }
503:
504: /**
505: * Starts the prover with a "BehaviouralSubtypingOp" proof obligation.
506: * @param subtype the UMLModelClass with the subtype for whose method
507: * behavioural subtyping has to be proven
508: * @return error message to the user
509: */
510: public static String proveBehaviouralSubtypingOp(
511: UMLModelClass subtype) {
512: //let the user select a supertype
513: SuperclassSelectionDialog dlg = new SuperclassSelectionDialog(
514: subtype);
515: if (!dlg.wasSuccessful()) {
516: return "";
517: }
518: ModelClass super type = dlg.getSuperclass();
519: if (super type == null) {
520: return "No supertype has been selected";
521: }
522:
523: //get all pairs of overriding and overridden operation contracts
524: //(if there are multiple contracts for one method in either
525: //the sub- or the supertype, this currently just pairs them in the order
526: //in which they appear; eventually, the user should be asked instead)
527: Map contractPairs = new HashMap();
528: Vector subOps = subtype.getOps();
529: Iterator it = subOps.iterator();
530: while (it.hasNext()) {
531: ModelMethod subMethod = (ModelMethod) (it.next());
532:
533: ModelMethod super Method = getOverriddenMethod(subMethod,
534: super type);
535: if (super Method != null) {
536: ListOfOperationContract subContracts = subMethod
537: .getMyOperationContracts();
538: ListOfOperationContract super Contracts = super Method
539: .getMyOperationContracts();
540: IteratorOfOperationContract subIt = subContracts
541: .iterator();
542: IteratorOfOperationContract super It = super Contracts
543: .iterator();
544: while (subIt.hasNext() && super It.hasNext()) {
545: contractPairs.put(subIt.next(), super It.next());
546: }
547: }
548: }
549: if (contractPairs.isEmpty()) {
550: return "No overridden contracts could be found "
551: + "in the selected supertype.";
552: }
553:
554: //create and start the PO
555: ProofOblInput po = new BehaviouralSubtypingOpPO(subtype,
556: super type, contractPairs);
557: return startProver(subtype, po);
558: }
559:
560: /**
561: * Starts the prover with a "StrongOperationContract" proof obligation.
562: * @param modelMethod the ModelMethod to reason about; the proof
563: * obligation will be about its *first* operation
564: * contract
565: * @return error message to the user
566: */
567: public static String proveStrongOperationContract(
568: ModelMethod modelMethod) {
569: //get the relevant contract
570: ListOfOperationContract contracts = modelMethod
571: .getMyOperationContracts();
572: if (contracts.isEmpty()) {
573: return "No contracts are available for the selected method.";
574: }
575: OperationContract contract = contracts.head();
576:
577: //let the user select the set of assumed invariants
578: ModelClass containingClass = modelMethod.getContainingClass();
579: Set modelClasses = containingClass.getAllClasses();
580:
581: ClassInvariantSelectionDialog dlg = new ClassInvariantSelectionDialog(
582: "Please select the assumed invariants", modelClasses,
583: false, containingClass);
584: if (!dlg.wasSuccessful()) {
585: return "";
586: }
587: ListOfClassInvariant assumedInvs = dlg.getClassInvariants();
588: if (assumedInvs.isEmpty()) {
589: return "No assumed invariants have been selected.";
590: }
591:
592: //let the user select the set of ensured invariants
593: dlg = new ClassInvariantSelectionDialog(
594: "Select ensured invariants", modelClasses, false,
595: containingClass);
596: if (!dlg.wasSuccessful()) {
597: return "";
598: }
599: ListOfClassInvariant ensuredInvs = dlg.getClassInvariants();
600: if (ensuredInvs.isEmpty()) {
601: return "No ensured invariants have been selected.";
602: }
603:
604: //create and start the PO
605: ProofOblInput po = new StrongOperationContractPO(contract,
606: assumedInvs, ensuredInvs);
607: return startProver(containingClass, po);
608: }
609:
610: /**
611: * Asks the user to choose a set of invariants and then starts the prover
612: * with a corresponding "PreservesInv" proof obligation.
613: * @param modelMethod the ModelMethod to reason about
614: * @return error message to the user
615: */
616: public static String provePreservesInv(ModelMethod modelMethod) {
617: ModelClass containingClass = modelMethod.getContainingClass();
618: Set modelClasses = modelMethod.getContainingClass()
619: .getAllClasses();
620:
621: //let the user select the set of ensured invariants
622: ClassInvariantSelectionDialog dlg = new ClassInvariantSelectionDialog(
623: "Please select the ensured invariants", modelClasses,
624: false, containingClass);
625: if (!dlg.wasSuccessful()) {
626: return "";
627: }
628: ListOfClassInvariant ensuredInvs = dlg.getClassInvariants();
629: if (ensuredInvs.isEmpty()) {
630: return "No ensured invariants have been selected.";
631: }
632:
633: //create and start the PO
634: ProofOblInput po = new PreservesInvPO(modelMethod, invStrategy,
635: ensuredInvs);
636: return startProver(containingClass, po);
637: }
638:
639: /**
640: * Starts the prover with a "PreservesOwnInv" proof obligation.
641: * @param modelMethod the ModelMethod to reason about
642: * @return error message to the user
643: */
644: public static String provePreservesOwnInv(ModelMethod modelMethod) {
645: if (modelMethod.getContainingClass().getMyClassInvariants()
646: .isEmpty()) {
647: return "No own invariants are available.";
648: }
649:
650: ProofOblInput po = new PreservesOwnInvPO(modelMethod,
651: invStrategy);
652: return startProver(modelMethod.getContainingClass(), po);
653: }
654:
655: public static String provePreservesThroughout(
656: ModelMethod modelMethod) {
657: ModelClass containingClass = modelMethod.getContainingClass();
658: Set modelClasses = modelMethod.getContainingClass()
659: .getAllClasses();
660:
661: //let the user select the set of throughout invariants
662: ClassInvariantSelectionDialog dlg = new ClassInvariantSelectionDialog(
663: "Please select the desired throughout invariants",
664: modelClasses, true, containingClass);
665: if (!dlg.wasSuccessful()) {
666: return "";
667: }
668: ListOfClassInvariant invariants = dlg.getClassInvariants();
669: if (invariants.isEmpty()) {
670: return "No throughout invariants have been selected.";
671: }
672:
673: //create and start the PO
674: ProofOblInput po = new PreservesThroughoutPO(modelMethod,
675: invariants, invStrategy);
676: return startProver(containingClass, po);
677: }
678:
679: /**
680: * Starts the prover with an "EnsuresPost" proof obligation.
681: * @param modelMethod the ModelMethod to reason about; the proof obligation
682: * will be about its *first* OperationContract
683: * @param modality the desired modality
684: * @return error message to the user
685: */
686: public static String proveEnsuresPost(ModelMethod modelMethod,
687: Modality modality) {
688: //get the relevant contract
689: ListOfOperationContract contracts = modelMethod
690: .getMyOperationContracts();
691: if (contracts.isEmpty()) {
692: return "No contracts are available for the selected method.";
693: }
694: OperationContract contract = contracts.head();
695:
696: //create and start the PO
697: ProofOblInput po = new EnsuresPostPO(contract, modality,
698: invStrategy);
699: return startProver(modelMethod.getContainingClass(), po);
700: }
701:
702: /**
703: * Starts the prover with a "RespectsModifies" proof obligation.
704: * @param modelMethod the ModelMethod to reason about; the proof obligation
705: * will be about its *first* OperationContract
706: * @return error message to the user
707: */
708: public static String proveRespectsModifies(ModelMethod modelMethod) {
709: //get the relevant contract
710: ListOfOperationContract contracts = modelMethod
711: .getMyOperationContracts();
712: if (contracts.isEmpty()) {
713: return "No contracts are available for the selected method.";
714: }
715: OperationContract contract = contracts.head();
716:
717: //create and start the PO
718: ProofOblInput po = new RespectsModifiesPO(contract, invStrategy);
719: return startProver(modelMethod.getContainingClass(), po);
720: }
721:
722: /**
723: * Starts the prover with an "IsGuard" proof obligation.
724: * @param modelMethod the ModelMethod to reason about
725: * @return error message to the user
726: */
727: public static String provePreservesGuard(ModelMethod modelMethod) {
728: ModelClass containingClass = modelMethod.getContainingClass();
729: Set modelClasses = containingClass.getAllClasses();
730:
731: //let the user select the guarded invariants
732: ClassInvariantSelectionDialog dlg = new ClassInvariantSelectionDialog(
733: "Please select the guarded invariants", modelClasses,
734: false, containingClass);
735: if (!dlg.wasSuccessful()) {
736: return "";
737: }
738: ListOfClassInvariant guardedInvs = dlg.getClassInvariants();
739: if (guardedInvs.isEmpty()) {
740: return "No guarded invariants have been selected.";
741: }
742:
743: //let the user select the guard classes
744: ListOfModelClass allClasses = SLListOfModelClass.EMPTY_LIST;
745: Iterator it = modelClasses.iterator();
746: while (it.hasNext()) {
747: allClasses = allClasses.prepend((UMLModelClass) it.next());
748: }
749: ClassSelectionDialog dlg2 = new ClassSelectionDialog(
750: "Please select the guard", "Available classes",
751: allClasses, containingClass, true);
752: if (!dlg2.wasSuccessful()) {
753: return "";
754: }
755: ListOfModelClass guard = dlg2.getSelection();
756: if (guard.isEmpty()) {
757: return "No guard classes have been selected.";
758: }
759:
760: //create the PO
761: ProofOblInput po = new PreservesGuardPO(modelMethod,
762: guardedInvs, guard, invStrategy);
763: return startProver(containingClass, po);
764: }
765: }
|