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: package de.uka.ilkd.key.counterexample;
012:
013: import de.uka.ilkd.key.logic.Axiom;
014: import de.uka.ilkd.key.logic.CExProblem;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.ldt.ADT;
017: import de.uka.ilkd.key.logic.op.ConstructorFunction;
018: import de.uka.ilkd.key.logic.sort.ArrayOfGenSort;
019: import de.uka.ilkd.key.logic.sort.GenSort;
020: import de.uka.ilkd.key.rule.TacletForTests;
021:
022: /**
023: * TestProgramm zum Testen des CounterExample Packages
024: * Achtung: sehr sehr gehackt, z.B. sind die Sorten in
025: * den Axiomen nicht dieselben wie die im ADT!!!!
026: */
027:
028: public class TestProgramm {
029:
030: CExProblem problem;
031: CounterExample gegenbeispiel;
032:
033: public TestProgramm(String filename, String ax, String conj) {
034:
035: //parsing stuff:
036: TacletForTests.parse(filename);
037: Axiom axiom = new Axiom(TacletForTests.parseTerm(ax));
038: Axiom conjecture = new Axiom(TacletForTests.parseTerm(conj));
039:
040: System.out.println("Axiom and conjecture successfully parsed.");
041:
042: //generating adt:
043: ADT adt = new ADT(new Name("NatAdt"));
044:
045: GenSort nat = new GenSort(new Name("NatSorte"));
046: GenSort[] gs = { nat };
047:
048: ArrayOfGenSort arg = new ArrayOfGenSort(gs);
049: ConstructorFunction cnull = new ConstructorFunction(new Name(
050: "null"), nat, null);
051: ConstructorFunction csucc = new ConstructorFunction(new Name(
052: "succ"), nat, arg);
053:
054: nat.addConstructor(cnull);
055: nat.addConstructor(csucc);
056:
057: System.out.println("Sort nat successfully generated.");
058:
059: adt.addSort(nat);
060: adt.addAxiom(axiom);
061:
062: System.out.println("Adt generation finished.");
063:
064: this .problem = new CExProblem(adt, conjecture);
065:
066: System.out.println("Starting CounterExample Generation");
067:
068: this .gegenbeispiel = new CounterExample(this .problem);
069:
070: }
071:
072: /**
073: * Following: the test programm which should output the
074: * results of the above functions if the programm does
075: * not crash with a runtime exception beforehand.
076: * first output should be the abstract data type and
077: * second output should be the counterexample ...
078: * while (not working) {
079: * if (output~(seems)~sensible) then { 'Hooray'; its = working }
080: * else { program some more }
081: * }
082: */
083:
084: public static void main(String[] args) {
085:
086: System.out.println("Dies ist das CounterExample Testprogramm");
087:
088: TestProgramm test = new TestProgramm("natstack.txt", args[0],
089: args[1]);
090:
091: System.out
092: .println("Der Test ist gelaufen, Ausgabe folgt unten:\n"
093: + test.problem.toString()
094: + "\n\n"
095: + test.gegenbeispiel.toString()
096: + "\n\n"
097: + "Ende ....");
098: }
099:
100: }
|