001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: //
011:
012: package de.uka.ilkd.key.counterexample;
013:
014: import de.uka.ilkd.key.logic.CExProblem;
015:
016: /**
017: * You can use this class to prove that a certain conjecture is wrong for an
018: * abstract data type. On initialization of CounterExample you can enter the
019: * problem which you want to test. Then you can generate the calculus and run
020: * the ModelGeneration Software Mgtp to get the CounterExample data.
021: *
022: * @author Sonja Pieper
023: * @see de.uka.ilkd.key.logic.CExProblem
024: * @version 1
025: * @since 10.08.2001
026: */
027:
028: public class CounterExample {
029:
030: private CExProblem problem;
031: private Calculus calculus;
032: private MgtpWrapper mgtp;
033: private ModelRepresentation model;
034:
035: static Configuration config = new Configuration("max");
036:
037: public CounterExample(CExProblem cexproblem) {
038: problem = cexproblem;
039: calculus = new ConjCalculus(problem);
040: mgtp = new MgtpWrapper(calculus);
041: model = new ModelRepresentation(mgtp.getProve());
042: }
043:
044: public CExProblem getProblem() {
045: return problem;
046: }
047:
048: public String getProblemString() {
049: return problem.toString();
050: }
051:
052: public Calculus getCalculus() {
053: return calculus;
054: }
055:
056: public String getCalculusString() {
057: return calculus.toString();
058: }
059:
060: public ModelRepresentation getModel() {
061: return model;
062: }
063:
064: public String getModelString() {
065: return model.toString();
066: }
067:
068: public String toString() {
069: String ausgabe = "\n\nCounter interpretation for the conjecture:\n"
070: + (this .problem.getConjecture()).toString()
071: + "\n\n\n"
072: + "Resulting term evaluation:\n\n"
073: + model.getTermeval()
074: + "\n"
075: + "The above interpretation satisfies the axioms,\n"
076: + "if instantiated by constructor terms with less then "
077: + (config.domainmax + 1)
078: + " constructors.\n"
079: + "\nSummary:\n"
080: + "\nThe conjecture "
081: + (this .problem.getConjecture()).toString()
082: + "\n\nis violated by the following variable assignment:\n"
083: + model.getVars()
084: + "\nand by the following evaluation of conjecture subterms:\n\n"
085: + model.getSubterms();
086: return ausgabe;
087: }
088:
089: /**
090: * This method allows to let the counter example generation proces
091: * start for a second time, with a newly generated calculus etc.
092: * might be useful after changing the configuration.
093: */
094: public void runAgain() {
095: calculus = new ConjCalculus(problem);
096: mgtp = new MgtpWrapper(calculus);
097: model = new ModelRepresentation(mgtp.getProve());
098: }
099:
100: public static void changeConfiguration() {
101: config.changeConfiguration();
102: }
103:
104: }
|