01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic.ldt;
12:
13: import java.util.Vector;
14:
15: import de.uka.ilkd.key.logic.Axiom;
16: import de.uka.ilkd.key.logic.Name;
17: import de.uka.ilkd.key.logic.Named;
18: import de.uka.ilkd.key.logic.sort.GenSort;
19: import de.uka.ilkd.key.logic.sort.Sort;
20:
21: /**
22: * This class represents an Abstract Data Type as needed for the
23: * generation of counterexamples. It consists of a name, 'freely'
24: * (simply assumed they are) generated sorts and axioms.
25: */
26:
27: public class ADT implements Named {
28:
29: private Vector sorts; //contains objects of type GenSort
30: private Vector axioms;//contains objects of type Axiom
31:
32: private Name name;
33:
34: /**
35: * creates a new empty ADT which is not yet useful, you will
36: * need to add sorts and axioms.
37: * @param n the Name of the constructor, can be anything it is
38: * simply needed as a kind of identifier
39: */
40: public ADT(Name n) {
41: name = n;
42: sorts = new Vector();
43: axioms = new Vector();
44: }
45:
46: /**
47: * creates a new ADT complete with sorts and axioms.
48: * @param n the name of the constructor
49: * @param s the vector with the generated sorts for this adt,
50: * all objects in this vector are supposed to be of Type GenSort
51: * @param a the vector with the axioms for this adt all objects in
52: * this vector are supposed to be of Type Axiom
53: */
54: public ADT(Name n, Vector s, Vector a) {
55: name = n;
56: sorts = new Vector(s);
57: axioms = new Vector(a);
58: }
59:
60: public Name name() {
61: return name;
62: }
63:
64: public void addSort(GenSort gs) {
65: sorts.addElement(gs);
66: }
67:
68: public void addSort(Sort s) {
69: sorts.addElement(s);
70: }
71:
72: public void addAxiom(Axiom a) {
73: axioms.addElement(a);
74: }
75:
76: public String toString() {
77: String s = new String();
78: return s;
79: }
80:
81: public Vector getSorts() {
82: return sorts;
83: }
84:
85: public Vector getAxioms() {
86: return axioms;
87: }
88:
89: }
|