| java.lang.Object
 de.uka.ilkd.key.rule.BoundUniquenessChecker
| BoundUniquenessChecker | | public class BoundUniquenessChecker (Code) | | The bound uniqueness checker ensures that schemavariables can be bound
at most once in the \find and \assumes part of a taclet. The justification for this restriction is to
prevent the user to write taclets that match only in very rare cases, e.g.
\assumes (==>\forall var; phi)
\find (\forall var; phi ==>)
would nearly never match, as var would be required to match
the same object.
|
| BoundUniquenessChecker | | public BoundUniquenessChecker(Sequent seq)(Code) | | |
| addAll | | public void addAll(Sequent seq)(Code) | | adds all formulas in the sequent to the list of terms to
include in the uniqueness check
Parameters:
seq - the Sequent with the formulas to add |
| addTerm | | public void addTerm(Term term)(Code) | | adds term to the list of terms to include in
the uniqueness check
Parameters:
term - a Term |
| correct | | public boolean correct()(Code) | | returns true if any variable is bound at most once in the
given set of terms
|
|
|