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;
12:
13: import de.uka.ilkd.key.logic.ldt.ADT;
14:
15: /**
16: * This class contains a an ADT and a conjecture and is the input for the call to Mgtp.
17: * The package de.uka.ilkd.key.counterexample uses this as input for the generation
18: * of the counterexample calculus which is then given as input to Mgtp. CEx stands
19: * for CounterExample
20: *
21: * @author Sonja Pieper
22: * @verions 0.1, 07/08/01
23: */
24:
25: public class CExProblem {
26:
27: private ADT datatype;
28: private Axiom conjecture;
29:
30: //@@@ the following 3 variables are maybe not necessary:
31: //private Namespace sorts;
32: //private Namespace functions;
33: //private Namespace variables;
34:
35: /**
36: * creates a new CExProblem, CEx stands for CounterExample
37: *
38: * @param dt the abstract data type with which you are working
39: * @param conj the conjecture which you want to disprove
40: */
41: public CExProblem(ADT dt, Axiom conj) {
42: datatype = dt;
43: conjecture = conj;
44: }
45:
46: /**
47: * constructor supposed to parse the necessary information
48: * from the filename given as parameter. a and c are an
49: * axiom and a conjecture for testing only now. @@@
50: */
51: /* public CExProblem(String filename, String a, String c){
52:
53: TacletForTests taclet = new TacletForTests();
54: taclet.parse(filename);
55: sorts = taclet.getSorts();
56: functions = taclet.getFunctions();
57: variables = taclet.getVariables();
58:
59: Axiom axiom = new Axiom(taclet.parseTerm(a)); //@@@
60:
61: String name = filename.substring(0,filename.indexOf('.')-1);
62: System.out.println("Dies ist der Name des neuen ADTs: "+name); //debug
63: datatype = new ADT(name);
64:
65: while(namespace!=null){
66: datatype.addSort(sorts);
67: }
68:
69: datatype.addAxiom(axiom);
70:
71: conjecture = new Axiom(taclet.parseTerm(c));
72:
73: }
74: */
75:
76: /**
77: * output of the object as a string
78: *
79: * @return the string representation of the object
80: */
81: public String toString() {
82: return datatype.toString() + "\n\n" + conjecture.toString();
83: }
84:
85: public ADT getAdt() {
86: return datatype;
87: }
88:
89: public Axiom getConjecture() {
90: return conjecture;
91: }
92:
93: }
|