| java.lang.Object
 de.uka.ilkd.key.counterexample.Calculus
de.uka.ilkd.key.counterexample.SortCalculus
All known Subclasses: de.uka.ilkd.key.counterexample.AxiomCalculus,
| SortCalculus | | public class SortCalculus extends Calculus (Code) | | This class generates the clauses which depend on the generated sorts,
it includes the static clauses generated by Calculus
which this class extends.
These clauses are different for each adt, depending on the generated
sorts that are used. To these belong the domain generation and search,
the rewriting of constructor arguments and the 'freely generated'
property clauses.
In the 'all' attribute inherited from Calculus are all Clauses
generated by the Calculus class, which means, that if you use an
instance of this class, you have both the static clauses of Calculus
and the Sort-dependent clauses of this class.
author:
Sonja Pieper
version:
0.1 |
| Method Summary | |
| public Clauses | getSortClauses()
This method returns a subset of the clauses of the complete
calculus, the clauses that generate the domain and search the domain,
constructor rewriting and the clauses that ensure the
adt's 'freely generated' generated property. |
| SortCalculus | | SortCalculus(Vector s)(Code) | | Creates a new instance of SortCalculus. First calls the
constructor of the super-class, the effect is that you
already have the static clauses in the all-List after that
is done. Afterwards all clauses SortCalculus generates
are added to the list.
Parameters:
s - The generated sorts of the adt are needed to generatethe clauses of this class |
| getSortClauses | | public Clauses getSortClauses()(Code) | | This method returns a subset of the clauses of the complete
calculus, the clauses that generate the domain and search the domain,
constructor rewriting and the clauses that ensure the
adt's 'freely generated' generated property.
The clauses that are dependent on knowing the adt's sorts. |
|
|