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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
011: // and Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016:
017: package de.uka.ilkd.key.parser;
018:
019: import java.io.PrintWriter;
020: import java.io.StringReader;
021: import java.io.StringWriter;
022:
023: import junit.framework.TestCase;
024: import de.uka.ilkd.key.java.Recoder2KeY;
025: import de.uka.ilkd.key.logic.*;
026: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
027: import de.uka.ilkd.key.logic.op.LogicVariable;
028: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
029: import de.uka.ilkd.key.logic.op.TermSymbol;
030: import de.uka.ilkd.key.logic.sort.Sort;
031: import de.uka.ilkd.key.pp.AbbrevMap;
032: import de.uka.ilkd.key.proof.init.InitConfig;
033: import de.uka.ilkd.key.proof.init.OCLInvSimplPO;
034: import de.uka.ilkd.key.rule.TacletForTests;
035:
036: public class TestTermParserOCL extends TestCase {
037:
038: private TermFactory tf = TermFactory.DEFAULT;
039: private NamespaceSet nss;
040: private Choice defaultChoice;
041: private Sort oclAny, oclBoolean;
042: private TermSymbol iterate, true_, false_, cons, nil, and, forAll,
043: oclWrapper;
044: private LogicVariable s, i;
045: private Term nilTerm, trueTerm, falseTerm;
046:
047: public TestTermParserOCL(String name) {
048: super (name);
049: }
050:
051: public void setUp() {
052: InitConfig initConf = new InitConfig();
053: OCLInvSimplPO.createNamespaceSetForTests(initConf);
054: nss = initConf.namespaces();
055:
056: forAll = (TermSymbol) initConf.funcNS().lookup(
057: new Name("$forAll"));
058: and = (TermSymbol) initConf.funcNS().lookup(new Name("$and"));
059: cons = (TermSymbol) initConf.funcNS().lookup(
060: new Name("$insert_set"));
061: nil = (TermSymbol) initConf.funcNS().lookup(
062: new Name("$empty_set"));
063: iterate = (TermSymbol) initConf.funcNS().lookup(
064: new Name("$iterate"));
065: true_ = (TermSymbol) initConf.funcNS()
066: .lookup(new Name("$true"));
067: false_ = (TermSymbol) initConf.funcNS().lookup(
068: new Name("$false"));
069: oclWrapper = (TermSymbol) initConf.funcNS().lookup(
070: new Name("$OclWrapper"));
071:
072: nilTerm = tf.createFunctionTerm(nil);
073: trueTerm = tf.createFunctionTerm(true_);
074: falseTerm = tf.createFunctionTerm(false_);
075: }
076:
077: private KeYParser stringTermParser(String s) {
078: return new KeYParser(
079: ParserMode.TERM,
080: new KeYLexer(new StringReader(s), null),
081: "No file. Call of parser from parser/TestTermParser.java",
082: tf, new Recoder2KeY(TacletForTests.services(), nss),
083: TacletForTests.services(), nss, new AbbrevMap());
084: }
085:
086: public Term parseTerm(String s) {
087: try {
088: KeYParser p = stringTermParser(s);
089: return p.term();
090: } catch (Exception e) {
091: StringWriter sw = new StringWriter();
092: PrintWriter pw = new PrintWriter(sw);
093: e.printStackTrace(pw);
094: throw new RuntimeException("Exc while Parsing:\n" + sw);
095: }
096: }
097:
098: //Tests OCL operators/operations without any bound variables
099: public void test1() {
100: Term term = tf.createFunctionTerm(and, trueTerm, falseTerm);
101: assertEquals("parse $and($true, $false)", term,
102: parseTerm("$and($true, $false)"));
103: }
104:
105: //Doesn't work as long as logic/Term::equals() checks "sort() == t.sorts()"
106: //instead of "sort().equals(t.sort())".
107:
108: //Tests OCL operations where one variable gets bound (forAll, exists, select, ...)
109: //Only for the problem clause of the .key file, where bound vars are treated as
110: //logical vars (not schema vars)
111: public void test2() {
112: Term tParse = parseTerm("$forAll($insert_set($true, $insert_set($false, $empty_set)),"
113: + "\\bind OclBoolean s; $and($true, s))");
114: LogicVariable this _s = (LogicVariable) tParse.varsBoundHere(1)
115: .getQuantifiableVariable(0);
116: ArrayOfQuantifiableVariable[] var = new ArrayOfQuantifiableVariable[2];
117: var[0] = new ArrayOfQuantifiableVariable(
118: new QuantifiableVariable[0]);
119: var[1] = new ArrayOfQuantifiableVariable(
120: new LogicVariable[] { this _s });
121: Term tS = tf.createVariableTerm(this _s);
122: Term t1Cons = tf.createFunctionTerm(cons, new Term[] {
123: falseTerm, nilTerm });
124: Term tCons = tf.createFunctionTerm(cons, new Term[] { trueTerm,
125: t1Cons });
126: Term tAnd = tf.createFunctionTerm(and, trueTerm, tS);
127: Term term = tf.createFunctionWithBoundVarsTerm(forAll,
128: new Term[] { tCons, tAnd }, var);
129: assertEquals(
130: "parse $forAll($insert_set($true, $insert_set($false, $empty_set)),"
131: + "\\bind OclBoolean s; $and($true, s))", term,
132: tParse);
133: }
134:
135: //Tests the OCL operation where two variables get bound -- iterate
136: //Only for the problem clause of the .key file, where bound vars are treated as
137: //logical vars (not schema vars)
138: public void test3() {
139: Term tParse = parseTerm("$iterate($insert_set($true, $insert_set($false, $empty_set)),"
140: + "$false, \\bind(OclBoolean s; OclBoolean acc) $and(s, acc))");
141: LogicVariable this _s = (LogicVariable) tParse.varsBoundHere(2)
142: .getQuantifiableVariable(0);
143: LogicVariable this _acc = (LogicVariable) tParse
144: .varsBoundHere(2).getQuantifiableVariable(1);
145: ArrayOfQuantifiableVariable[] var = new ArrayOfQuantifiableVariable[3];
146: var[0] = new ArrayOfQuantifiableVariable(
147: new QuantifiableVariable[0]);
148: var[1] = new ArrayOfQuantifiableVariable(
149: new QuantifiableVariable[0]);
150: var[2] = new ArrayOfQuantifiableVariable(new LogicVariable[] {
151: this _s, this _acc });
152: Term tS = tf.createVariableTerm(this _s);
153: Term tAcc = tf.createVariableTerm(this _acc);
154: Term t1Cons = tf.createFunctionTerm(cons, new Term[] {
155: falseTerm, nilTerm });
156: Term tCons = tf.createFunctionTerm(cons, new Term[] { trueTerm,
157: t1Cons });
158: Term tAnd = tf.createFunctionTerm(and, tS, tAcc);
159: Term term = tf.createFunctionWithBoundVarsTerm(iterate,
160: new Term[] { tCons, falseTerm, tAnd }, var);
161: assertEquals(
162: "parse $iterate($insert_set($true, $insert_set($false, $empty_set)),"
163: + "$false, \\bind(OclBoolean s; OclBoolean acc) $and(s, acc))",
164: term, tParse);
165: }
166:
167: }
|