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:
12: package de.uka.ilkd.key.counterexample;
13:
14: import de.uka.ilkd.key.logic.CExProblem;
15:
16: /**
17: * An instance of this class contains the fully generated calculus including all components generated througout the inherited classes: static clauses, sort dependent clauses, clauses generated from axioms and the clause representing the conjecture.
18: * @author Sonja Pieper
19: * @version 0.1
20: * @see Calculus
21: */
22: public class ConjCalculus extends AxiomCalculus {
23:
24: CExProblem problem;
25: Clauses conjecture;
26:
27: public ConjCalculus(CExProblem cep) {
28: super (cep.getAdt());
29: problem = cep;
30:
31: conjecture = new Clauses(); //@@@
32: this .all.add(conjecture);
33: }
34:
35: public Clauses getConjectureClause() {
36: return conjecture;
37: }
38: }
|