|
Used for OCL Simplification, i.e. not for usual logic terms.
The operators in this package
makes it possible to build OCL expressions in the form of
{@link de.uka.ilkd.key.logic.Term}s, with the ultimate goal of
applying simplification taclets to these {@link de.uka.ilkd.key.logic.Term}s
and then pretty-print the simplified expressions back to usual
OCL syntax again.
Most of the pre-defined OCL operations can be expressed using
{@link de.uka.ilkd.key.logic.op.Function}, but some of them
need more complex operators. These more complex
operators are collected in this package. There is also in this
package a class {@link de.uka.ilkd.key.logic.op.oclop.OclOp} containing
all pre-defined OCL operations, also the ones based on
{@link de.uka.ilkd.key.logic.op.Function}, in form of constants.
The operators defined in this package all extend
{@link de.uka.ilkd.key.logic.op.TermSymbol}.
One thing that makes {@link de.uka.ilkd.key.logic.op.Function}
inappropriate to use for some OCL operations is the fact
that it assumes that the type/sort of a term is only dependent
on its top-level operator, while in OCL the type of an
expression can also depend on its sub expressions. For example:
collection->iterate(elem ; acc:T=init_expr | expr_with_elem_and_acc)
The type of this expression is determined by the type of the
accumulator acc.
Last modified: Thu Jan 27 10:13:36 MET 2005
|