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.rule;
012:
013: import java.io.PrintWriter;
014: import java.io.StringReader;
015: import java.io.StringWriter;
016:
017: import junit.framework.TestCase;
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.*;
020: import de.uka.ilkd.key.logic.op.*;
021: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
022: import de.uka.ilkd.key.logic.sort.Sort;
023: import de.uka.ilkd.key.parser.KeYLexer;
024: import de.uka.ilkd.key.parser.KeYParser;
025: import de.uka.ilkd.key.parser.ParserMode;
026:
027: /**
028: * create Taclet for test cases.
029: */
030: public class CreateTacletForTests extends TestCase {
031:
032: Sort nat;
033:
034: public static AntecTaclet impleft;
035: public static SuccTaclet impright;
036: public static SuccTaclet imprightadd;
037: public static AntecTaclet notleft;
038: public static SuccTaclet notright;
039: public static SuccTaclet close;
040: public static SuccTaclet allright;
041: public static AntecTaclet allleft;
042: public static RewriteTaclet contradiction;
043: public static NoFindTaclet cut;
044: public static RewriteTaclet predsuccelim;
045: public static RewriteTaclet pluszeroelim;
046: public static RewriteTaclet zeropluselim;
047: public static RewriteTaclet succelim;
048: public static RewriteTaclet switchsecondsucc;
049: public static RewriteTaclet switchfirstsucc;
050: public static SuccTaclet closewitheq;
051:
052: static Function func_0;
053: static Function func_eq;
054: static Function func_plus;
055: static Function func_min1;
056: static Function func_plus1;
057: static Function func_p; // Sort.FORMULA
058:
059: static Sequent seq_test1;
060: static Sequent seq_test2;
061: static Sequent seq_test3;
062: public static Sequent seq_testNat;
063: static Sequent seq_testAll;
064:
065: static SchemaVariable b;
066: static SchemaVariable x;
067: static SchemaVariable x0;
068: static SchemaVariable t0;
069: static LogicVariable z;
070: static Sort sort1;
071: static TermFactory tf = TermFactory.DEFAULT;
072:
073: static NamespaceSet nss;
074:
075: public Services services;
076:
077: public CreateTacletForTests(String name) {
078: super (name);
079: services = new Services();
080: }
081:
082: public void createTaclets() {
083: impleft = (AntecTaclet) parseTaclet("imp_left{\\find(b->b0==>) \\replacewith(b0==>); \\replacewith(==> b)}");
084: impright = (SuccTaclet) parseTaclet("imp_right{\\find(==> b->b0) \\replacewith(b ==> b0)}");
085: notleft = (AntecTaclet) parseTaclet("not_left{\\find(not b==>) \\replacewith(==>b)}");
086: notright = (SuccTaclet) parseTaclet("not_right{\\find(==>not b) \\replacewith(b==>)}");
087: cut = (NoFindTaclet) parseTaclet("cut{\\add(b==>); \\add(==>b)}");
088: imprightadd = (SuccTaclet) parseTaclet("imp_right_add{\\find(==> b->b0) \\replacewith(b==>b0) \\addrules("
089: + "cut{\\add(b==>); \\add(==>b)})}");
090: close = (SuccTaclet) parseTaclet("close_goal{\\assumes (b==>) \\find(==>b) \\closegoal}");
091: contradiction = (RewriteTaclet) parseTaclet("contracdiction{\\find(b->b0) \\replacewith(!b0 -> !b)}");
092: allright = (SuccTaclet) parseTaclet("all_right{\\find (==> \\forall z; b) \\varcond ( \\new(x,\\dependingOn(b)) ) \\replacewith (==> {\\subst z; x}b)}");
093: allleft = (AntecTaclet) parseTaclet("all_left{\\find(\\forall z; b==>) \\add({\\subst z; x}b==>)}");
094:
095: }
096:
097: public void createNatTaclets() {
098: //decls for nat
099: func_0 = new RigidFunction(new Name("zero"), nat, new Sort[] {});
100: func_eq = new RigidFunction(new Name("="), Sort.FORMULA,
101: new Sort[] { nat, nat });
102: func_plus = new RigidFunction(new Name("+"), nat, new Sort[] {
103: nat, nat });
104: func_min1 = new RigidFunction(new Name("pred"), nat,
105: new Sort[] { nat });
106: func_plus1 = new RigidFunction(new Name("succ"), nat,
107: new Sort[] { nat });
108:
109: nss.functions().add(func_0);
110: nss.functions().add(func_eq);
111: nss.functions().add(func_plus);
112: nss.functions().add(func_min1);
113: nss.functions().add(func_plus1);
114:
115: SchemaVariable var_rn = SchemaVariableFactory.createTermSV(
116: new Name("rn"), nat, false);
117: SchemaVariable var_rm = SchemaVariableFactory.createTermSV(
118: new Name("rm"), nat, false);
119:
120: Term t_rn = tf.createFunctionTerm(
121: (SortedSchemaVariable) var_rn, new Term[] {});
122: Term t_rm = tf.createFunctionTerm(
123: (SortedSchemaVariable) var_rm, new Term[] {});
124: Term t_0 = tf.createFunctionTerm(func_0, new Term[] {});
125: Term t_rnminus1 = tf.createFunctionTerm(func_min1,
126: new Term[] { t_rn });
127: Term t_rnminus1plus1 = tf.createFunctionTerm(func_plus1,
128: new Term[] { t_rnminus1 });
129: Term t_rneq0 = tf.createFunctionTerm(func_eq, new Term[] {
130: t_rn, t_0 });
131: // Term t_0minus1=tf.createFunctionTerm(func_min1,
132: // new Term[]{t_0});
133: Term t_0plus1 = tf.createFunctionTerm(func_plus1,
134: new Term[] { t_0 });
135:
136: // help rule r1: find(rn) replacewith(0) replacewith(0)
137: RewriteTacletBuilder rwb1 = new RewriteTacletBuilder();
138: rwb1.setName(new Name("r1"));
139: rwb1.setFind(t_rn);
140: rwb1.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
141: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST, t_0));
142:
143: //pred-succ-elim-rule
144: // find(rn -1 +1) replacewith(rn) replacewith(0 +1) addrule(r1)
145: RewriteTacletBuilder rwbuilder = new RewriteTacletBuilder();
146: rwbuilder.setFind(t_rnminus1plus1);
147: rwbuilder
148: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
149: Sequent.EMPTY_SEQUENT,
150: SLListOfTaclet.EMPTY_LIST, t_rn));
151: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
152: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST
153: .prepend(rwb1.getTaclet()), t_0plus1));
154: rwbuilder.setName(new Name("pred-succ-elim"));
155: pluszeroelim = rwbuilder.getRewriteTaclet();
156:
157: //plus-zero-elim
158: // find(rn + 0) replacewith(rn)
159: rwbuilder = new RewriteTacletBuilder();
160: rwbuilder.setFind(tf.createFunctionTerm(func_plus, new Term[] {
161: t_rn, t_0 }));
162: rwbuilder
163: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
164: Sequent.EMPTY_SEQUENT,
165: SLListOfTaclet.EMPTY_LIST, t_rn));
166: rwbuilder.setName(new Name("plus-zero-elim"));
167: predsuccelim = rwbuilder.getRewriteTaclet();
168:
169: //zero-plus-elim
170: // find(0 + rn) replacewith(rn)
171: rwbuilder = new RewriteTacletBuilder();
172: rwbuilder.setFind(tf.createFunctionTerm(func_plus, new Term[] {
173: t_0, t_rn }));
174: rwbuilder
175: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
176: Sequent.EMPTY_SEQUENT,
177: SLListOfTaclet.EMPTY_LIST, t_rn));
178: rwbuilder.setName(new Name("zero-plus-elim"));
179: zeropluselim = rwbuilder.getRewriteTaclet();
180:
181: //closewitheq
182: // find(=> rn=rn)
183: SuccTacletBuilder sbuilder = new SuccTacletBuilder();
184: Term t_rneqrn = tf.createFunctionTerm(func_eq, new Term[] {
185: t_rn, t_rn });
186: sbuilder.setFind(t_rneqrn);
187: sbuilder.setName(new Name("close-with-eq"));
188: closewitheq = sbuilder.getSuccTaclet();
189:
190: //switch first succ
191: // find((rn +1) + rm) replacewith((rn + rm) +1)
192: Term t_rnplus1 = tf.createFunctionTerm(func_plus1,
193: new Term[] { t_rn });
194: Term t_rnplus1plusrm = tf.createFunctionTerm(func_plus,
195: new Term[] { t_rnplus1, t_rm });
196:
197: Term t_rnplusrm = tf.createFunctionTerm(func_plus, new Term[] {
198: t_rn, t_rm });
199: Term t_rnplusrmplus1 = tf.createFunctionTerm(func_plus1,
200: new Term[] { t_rnplusrm });
201:
202: rwbuilder = new RewriteTacletBuilder();
203: rwbuilder.setFind(t_rnplus1plusrm);
204: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
205: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
206: t_rnplusrmplus1));
207: rwbuilder.setName(new Name("switch-first-succ"));
208: switchfirstsucc = rwbuilder.getRewriteTaclet();
209:
210: //switch second succ
211: // find(rn + (rm +1)) replacewith((rn + rm) +1)
212: Term t_rmplus1 = tf.createFunctionTerm(func_plus1,
213: new Term[] { t_rm });
214: Term t_rnplus_rmplus1 = tf.createFunctionTerm(func_plus,
215: new Term[] { t_rn, t_rmplus1 });
216: rwbuilder = new RewriteTacletBuilder();
217: rwbuilder.setFind(t_rnplus_rmplus1);
218: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
219: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
220: t_rnplusrmplus1));
221: rwbuilder.setName(new Name("switch-second-succ"));
222: switchsecondsucc = rwbuilder.getRewriteTaclet();
223:
224: //elim-succ
225: // find(rn +1 = rm +1) replacewith(rn=rm)
226: Term t_rneqrm = tf.createFunctionTerm(func_eq, new Term[] {
227: t_rn, t_rm });
228: rwbuilder = new RewriteTacletBuilder();
229: rwbuilder.setFind(tf.createFunctionTerm(func_eq, new Term[] {
230: t_rnplus1, t_rmplus1 }));
231: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
232: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
233: t_rneqrm));
234: rwbuilder.setName(new Name("succ-elim"));
235: succelim = rwbuilder.getRewriteTaclet();
236:
237: }
238:
239: public void setUp() {
240: nss = new NamespaceSet();
241:
242: parseDecls("\\sorts { Nat; testSort1; }\n"
243: + "\\schemaVariables {\n" + " \\formula b,b0;\n"
244: + " \\term testSort1 x;\n"
245: + " \\variables testSort1 z;\n" + "}\n");
246:
247: sort1 = (Sort) nss.sorts().lookup(new Name("testSort1"));
248: nat = (Sort) nss.sorts().lookup(new Name("Nat"));
249:
250: b = (SchemaVariable) nss.variables().lookup(new Name("b"));
251:
252: // createTaclets
253: createTaclets();
254: createNatTaclets();
255:
256: // problem
257:
258: String test1 = "\\predicates {A; B; } (A -> B) -> (!(!(A -> B)))";
259: Term t_test1 = null;
260: try {
261: StringReader fr = new StringReader(test1);
262: KeYParser parser = new KeYParser(ParserMode.PROBLEM,
263: new KeYLexer(fr, null));
264: t_test1 = parser.problem();
265: } catch (Exception e) {
266: System.err.println("Parser Error or Input Error");
267: fail("Parser Error");
268: }
269: ConstrainedFormula cf = new ConstrainedFormula(t_test1,
270: Constraint.BOTTOM);
271: ConstrainedFormula cf2 = new ConstrainedFormula(t_test1,
272: Constraint.BOTTOM);
273: seq_test1 = Sequent.createSequent(
274: Semisequent.EMPTY_SEMISEQUENT,
275: Semisequent.EMPTY_SEMISEQUENT.insert(0, cf)
276: .semisequent());
277: seq_test2 = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
278: .insert(0, cf).semisequent(),
279: Semisequent.EMPTY_SEMISEQUENT);
280: seq_test3 = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
281: .insert(0, cf).semisequent(),
282: Semisequent.EMPTY_SEMISEQUENT.insert(0, cf2)
283: .semisequent());
284:
285: func_p = new RigidFunction(new Name("P"), Sort.FORMULA,
286: new Sort[] { sort1 });
287: nss.functions().add(func_p);
288:
289: //nat problem:
290: Function const_c = new RigidFunction(new Name("c"), nat,
291: new PrimitiveSort[0]);
292: nss.functions().add(const_c);
293: Function const_d = new RigidFunction(new Name("d"), nat,
294: new PrimitiveSort[0]);
295: nss.functions().add(const_d);
296:
297: Term t_c = tf.createFunctionTerm(const_c, new Term[] {});
298: Term t_d = tf.createFunctionTerm(const_d, new Term[] {});
299: Term t_cplusd = tf.createFunctionTerm(func_plus, new Term[] {
300: t_c, t_d });
301: Term t_dminus1 = tf.createFunctionTerm(func_min1,
302: new Term[] { t_d });
303: Term t_dminus1plus1 = tf.createFunctionTerm(func_plus1,
304: new Term[] { t_dminus1 });
305: Term t_dminus1plus1plusc = tf.createFunctionTerm(func_plus,
306: new Term[] { t_dminus1plus1, t_c });
307: Term t_eq1 = tf.createFunctionTerm(func_eq, new Term[] {
308: t_cplusd, t_dminus1plus1plusc });
309:
310: Term t_cplus1 = tf.createFunctionTerm(func_plus1,
311: new Term[] { t_c });
312: Term t_cplus1plusd = tf.createFunctionTerm(func_plus,
313: new Term[] { t_cplus1, t_d });
314: Term t_dpluscplus1 = tf.createFunctionTerm(func_plus,
315: new Term[] { t_d, t_cplus1 });
316: Term t_eq2 = tf.createFunctionTerm(func_eq, new Term[] {
317: t_cplus1plusd, t_dpluscplus1 });
318: Term tnat = tf.createJunctorTerm(Op.IMP, t_eq1, t_eq2);
319:
320: // => (c+d) = ((d -1 +1) +c) -> (c +1)+d = (d+c) +1
321: seq_testNat = Sequent.createSequent(
322: Semisequent.EMPTY_SEMISEQUENT,
323: Semisequent.EMPTY_SEMISEQUENT
324: .insert(
325: 0,
326: new ConstrainedFormula(tnat,
327: Constraint.BOTTOM))
328: .semisequent());
329:
330: z = new LogicVariable(new Name("z"), sort1);
331: Term t_z = tf.createFunctionTerm(z, new Term[0]);
332: Term t_allzpz = tf.createQuantifierTerm(Op.ALL,
333: new LogicVariable[] { z }, tf.createFunctionTerm(
334: func_p, new Term[] { t_z }));
335: ConstrainedFormula cf3 = new ConstrainedFormula(t_allzpz,
336: Constraint.BOTTOM);
337: seq_testAll = Sequent.createSequent(
338: Semisequent.EMPTY_SEMISEQUENT,
339: Semisequent.EMPTY_SEMISEQUENT.insert(0, cf3)
340: .semisequent());
341:
342: }
343:
344: private KeYParser stringDeclParser(String s) {
345: return new KeYParser(
346: ParserMode.DECLARATION,
347: new KeYLexer(new StringReader(s), null),
348: "No file. CreateTacletForTests.stringParser(" + s + ")",
349: services, nss);
350: }
351:
352: public void parseDecls(String s) {
353: try {
354: KeYParser p = stringDeclParser(s);
355: p.decls();
356: } catch (Exception e) {
357: StringWriter sw = new StringWriter();
358: PrintWriter pw = new PrintWriter(sw);
359: e.printStackTrace(pw);
360: throw new RuntimeException("Exc while Parsing:\n" + sw);
361: }
362: }
363:
364: private KeYParser stringTacletParser(String s) {
365: return new KeYParser(
366: ParserMode.TACLET,
367: new KeYLexer(new StringReader(s), null),
368: "No file. CreateTacletForTests.stringParser(" + s + ")",
369: tf, services, nss);
370: }
371:
372: Taclet parseTaclet(String s) {
373: try {
374: KeYParser p = stringTacletParser(s);
375:
376: return p.taclet(SetAsListOfChoice.EMPTY_SET);
377: } catch (Exception e) {
378: StringWriter sw = new StringWriter();
379: PrintWriter pw = new PrintWriter(sw);
380: e.printStackTrace(pw);
381: throw new RuntimeException("Exc while Parsing:\n" + sw);
382: }
383: }
384:
385: }
|