| de.uka.ilkd.key.gui.JMLPOAndSpecProvider
All known Subclasses: de.uka.ilkd.key.gui.JMLEclipseAdapter,
JMLPOAndSpecProvider | public interface JMLPOAndSpecProvider (Code) | | |
createPOandStartProver | void createPOandStartProver(JMLSpec spec, boolean allInv, boolean invPost, boolean assignable)(Code) | | Creates a proof obligation for spec .
Parameters: allInv - true iff it should be assumed that every invariant ofevery class holds for all existing object in the prestate of the methodthat is specified by spec . Parameters: invPost - if true, the applicable invariants are added to the postcondition. Parameters: assignable - if true, a proof obligation for the assignable clauseof spec is created. |
|
|