| java.lang.Object
 de.uka.ilkd.key.logic.ldt.ADT
All known Subclasses: de.uka.ilkd.key.logic.ldt.LDT,
| ADT | | public class ADT implements Named(Code) | | This class represents an Abstract Data Type as needed for the
generation of counterexamples. It consists of a name, 'freely'
(simply assumed they are) generated sorts and axioms.
|
| Constructor Summary | |
| public | ADT(Name n)
creates a new empty ADT which is not yet useful, you will
need to add sorts and axioms. | | public | ADT(Name n, Vector s, Vector a)
creates a new ADT complete with sorts and axioms. |
| ADT | | public ADT(Name n)(Code) | | creates a new empty ADT which is not yet useful, you will
need to add sorts and axioms.
Parameters:
n - the Name of the constructor, can be anything it is simply needed as a kind of identifier |
| ADT | | public ADT(Name n, Vector s, Vector a)(Code) | | creates a new ADT complete with sorts and axioms.
Parameters:
n - the name of the constructor
Parameters:
s - the vector with the generated sorts for this adt,all objects in this vector are supposed to be of Type GenSort
Parameters:
a - the vector with the axioms for this adt all objects in this vector are supposed to be of Type Axiom |
|
|