public class BoundUniquenessChecker
extends java.lang.Object
\assumes (==>\forall var; phi)
\find (\forall var; phi ==>)
would nearly never match, as var would be required to match
the same object.Constructor and Description |
---|
BoundUniquenessChecker(Sequent seq) |
BoundUniquenessChecker(Term t,
Sequent seq) |
Modifier and Type | Method and Description |
---|---|
void |
addAll(Sequent seq)
adds all formulas in the sequent to the list of terms to
include in the uniqueness check
|
void |
addTerm(Term term)
adds term to the list of terms to include in
the uniqueness check
|
boolean |
correct()
returns true if any variable is bound at most once in the
given set of terms
|
public BoundUniquenessChecker(Sequent seq)
public void addTerm(Term term)
term
- a Termpublic void addAll(Sequent seq)
seq
- the Sequent with the formulas to addpublic boolean correct()
Copyright © 2003-2019 The KeY-Project.