| de.uka.ilkd.key.proof.init.OCLSimplificationPO
All known Subclasses: de.uka.ilkd.key.proof.init.OCLInvSimplPO,
| OCLSimplificationPO | | public interface OCLSimplificationPO (Code) | | Proof obligations resulting from the OCL Simplification implement this interface.
Currently the main reason is to avoid some dependencies on Together OpenAPI which
make it impossible to compile KeY without Together.
|
| Method Summary | |
| void | createNamespaceSet(InitConfig initConf)
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. |
| createNamespaceSet | | 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. |
|
|