| java.lang.Object
 de.uka.ilkd.key.parser.jml.JMLSpecBuilder
| JMLSpecBuilder | | public class JMLSpecBuilder (Code) | | provides methods for parsing the specifications of a single class/interface.
|
| buildProofObligation | | public Term buildProofObligation(ProgramMethod pm)(Code) | | returns a term containing the proofobligations for the methodspecs
of pm and the invariant and constraint proofobligation
for the containing class.
|
| buildProofObligations | | public HashMap buildProofObligations() throws ProofInputException(Code) | | returns a mapping from methods to terms that are conjunctions
of the proofobligations generated from the methodspecs of these methods
obsolete (but for testing reasons still there).
|
| getMethod2Specs | | public HashMap getMethod2Specs()(Code) | | returns a map from methods to the specs which have been parsed by this
JMLSpecBuilder.
|
| getModelMethod2Specs | | public HashMap getModelMethod2Specs()(Code) | | returns a map with the model methods and their specs
parsed by this JMLSpecBuilder.
|
| parseJMLClassSpec | | public void parseJMLClassSpec() throws ProofInputException(Code) | | parses jml specification like invariants, constraints or represents
in cd. parseModelMethodDecls() and parseModelFieldDecls()
have to be called first.
|
| parseJMLMethodSpecs | | public void parseJMLMethodSpecs() throws ProofInputException(Code) | | Parses the specs of the methods declared in cd
|
| parseModelFieldDecls | | public void parseModelFieldDecls() throws ProofInputException(Code) | | parses jml model fields declared in cd.
Can't be called before parseModelMethodDecls() has been called
|
| parseModelMethodDecls | | public void parseModelMethodDecls() throws ProofInputException(Code) | | parses jml model methods declared in cd.
|
|
|