| de.uka.ilkd.key.jml.JMLLemmaMethodSpec
All known Subclasses: de.uka.ilkd.key.jml.JMLMethodSpec,
| JMLLemmaMethodSpec | | public interface JMLLemmaMethodSpec (Code) | | Methodspecs which implement this interface can be used for generating
lemmas.
|
| getCompletePost | | Term getCompletePost(boolean withClassSpec, boolean allInv)(Code) | | returns postcondition with represents relations applied
|
| getCompletePre | | Term getCompletePre(boolean withClassSpec, boolean allInv, boolean terminationCase)(Code) | | returns precondition with represents relations applied
|
| getOldLVs | | ListOfQuantifierPrefixEntry getOldLVs()(Code) | | returns the variables used for the specification of \old<\code>
|
| getPi1 | | Term getPi1()(Code) | | returns the "\old<\code>-equations"
|
| getProofStatement | | ProgramElement getProofStatement()(Code) | | returns the ProgramElement used in the findpart of the lemmataclet
|
| replaceModelFieldsInAssignable | | SetOfLocationDescriptor replaceModelFieldsInAssignable()(Code) | | returns the modifies clause
|
| terminates | | boolean terminates()(Code) | | returns true iff the specification demands termination (normally or by
throwing an exception).
|
|
|