| java.lang.Object
 de.uka.ilkd.key.proof.init.OCLProofOblInput
de.uka.ilkd.key.proof.init.OCLInvSimplPO
| OCLInvSimplPO | | public class OCLInvSimplPO extends OCLProofOblInput implements OCLSimplificationPO(Code) | | Used for OCL Simplification.
Consists of two separate parts (and should probably be divided
into two classes):
- One part is responsible for adding the needed sorts and functions
to the namespaces (InitConfig) used by the prover.
- The other part creates, given a model representation of
a class, a proof obligation of its invariant in the form
of a term.
The first step is to translate the OCL syntax to a representation
expressed in the taclet language. This is done using the external
program "ocl2taclet". The next step is then to apply the taclet
parser to this representation, and the result is a Term
representation of the invariant. This term becomes a proof
obligation and can be handled by the prover.
|
| createNamespaceSet | | public void createNamespaceSet(InitConfig initConf)(Code) | | Adds OCL types, OCL operations, and model properties to the
name spaces of the initial configuration.
Can as well be hard-coded, since they are needed for all
OCL simplification. Also avoids trouble with taclet parser.
Parameters:
initConf - The initial configuration whose set of namespaces needs to be updated. |
| createNamespaceSetForTests | | public static void createNamespaceSetForTests(InitConfig initConf)(Code) | | |
| generateInvSimplPO | | protected Term generateInvSimplPO()(Code) | | Extracts the String invariant of the class representation,
turns it into a corresponding Term, and wraps it in some
other operators so that it can be handled by the prover.
Resulting Term. |
| prepareInv | | protected String prepareInv(ModelClass aClass)(Code) | | Extracts the String invariant from the class representation
and rewrites it into a format accepted by the "ocl2taclet"
parser program.
|
| readProblem | | public void readProblem(ModStrategy mod)(Code) | | Creates and sets the proof obligation term.
|
| setProofObligation | | protected void setProofObligation(Term po)(Code) | | |
|
|