|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.AbstractMetaOperator
de.uka.ilkd.key.rule.metaconstruct.WhileInvRule
| WhileInvRule | | public WhileInvRule()(Code) | | |
| neededInstantiations | | public ListOfSchemaVariable neededInstantiations(ProgramElement originalLoop, SVInstantiations svInst)(Code) | | returns the schemavariables that are needed to transform the given
loop. The unwind-loop construct may need labels if unlabeled breaks
and/or continues occur in the loop. Often there will be uninstantiated
Schemavariables in the loop that is why the found instantiations have to
be given.
|
| sort | | public Sort sort(Term[] term)(Code) | | Unlike other meta operators this one returns a formula
not a term.
|
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator. The
assumption that the top level operator and the term are equal
is NOT checked.
true iff the top level structure ofthe @link Term is valid. |
|
|
|