01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.gui;
12:
13: import java.util.Vector;
14:
15: import de.uka.ilkd.key.collection.ListOfString;
16: import de.uka.ilkd.key.jml.JMLSpec;
17:
18: public interface JMLPOAndSpecProvider {
19:
20: Vector getMethodSpecs(String className, String methodName,
21: ListOfString signature);
22:
23: /**
24: * Creates a proof obligation for <code>spec</code>.
25: * @param allInv true iff it should be assumed that every invariant of
26: * every class holds for all existing object in the prestate of the method
27: * that is specified by <code>spec</code>.
28: * @param invPost if true, the applicable invariants are added to the
29: * postcondition.
30: * @param assignable if true, a proof obligation for the assignable clause
31: * of <code>spec</code> is created.
32: */
33: void createPOandStartProver(JMLSpec spec, boolean allInv,
34: boolean invPost, boolean assignable);
35:
36: }
|