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.File;
014:
015: import junit.framework.TestCase;
016: import de.uka.ilkd.key.logic.*;
017: import de.uka.ilkd.key.logic.op.Function;
018: import de.uka.ilkd.key.logic.op.Op;
019: import de.uka.ilkd.key.logic.op.SchemaVariable;
020: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
021: import de.uka.ilkd.key.util.HelperClassForTests;
022:
023: /**
024: * class tests the building of Taclets in TacletBuilders, especially the
025: * checking if the SchemaVariables fulfill certain conditions. They must
026: * not occur more than once in find and if taken as a whole. Is obviously
027: * quite incomplete.
028: */
029:
030: public class TestTacletBuild extends TestCase {
031:
032: public static final Term[] NO_SUBTERMS = new Term[0];
033:
034: TermFactory tf = TermFactory.DEFAULT;
035:
036: public TestTacletBuild(String name) {
037: super (name);
038: }
039:
040: public void setUp() {
041: TacletForTests.setStandardFile(TacletForTests.testRules);
042: TacletForTests.parse();
043: }
044:
045: public void test0() {
046: SortedSchemaVariable u = (SortedSchemaVariable) TacletForTests
047: .getVariables().lookup(new Name("u"));
048: SortedSchemaVariable v = (SortedSchemaVariable) TacletForTests
049: .getVariables().lookup(new Name("v"));
050: Term b = tf.createFunctionTerm(
051: (SortedSchemaVariable) TacletForTests.getVariables()
052: .lookup(new Name("b")), NO_SUBTERMS);
053: Term t1 = tf.createQuantifierTerm(Op.EX, u, b);
054: Term t2 = tf.createQuantifierTerm(Op.EX, v, b);
055: RewriteTacletBuilder sb = new RewriteTacletBuilder();
056: sb.setFind(t1);
057: sb.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
058: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST, t2));
059: boolean thrown = false;
060: try {
061: sb.getTaclet();
062: } catch (RuntimeException e) {
063: thrown = true;
064: }
065: assertTrue(
066: "An exception should be thrown as there are different "
067: + "prefixes at different occurrences", thrown);
068: sb.addVarsNotFreeIn(u, (SchemaVariable) b.op());
069: sb.addVarsNotFreeIn(v, (SchemaVariable) b.op());
070: sb.getTaclet(); //no exception is thrown here anymore
071:
072: }
073:
074: public void testUniquenessOfIfAndFindVarSVsInIfAndFind() {
075: boolean thrown = false;
076: SortedSchemaVariable u = (SortedSchemaVariable) TacletForTests
077: .getVariables().lookup(new Name("u"));
078: Term A = tf.createFunctionTerm((Function) TacletForTests
079: .getFunctions().lookup(new Name("A")), NO_SUBTERMS);
080: Term t1 = tf.createQuantifierTerm(Op.ALL, u, A);
081: Sequent seq = Sequent
082: .createSuccSequent(Semisequent.EMPTY_SEMISEQUENT
083: .insert(0, new ConstrainedFormula(t1))
084: .semisequent());
085: Term t2 = tf.createQuantifierTerm(Op.EX, u, A);
086: SuccTacletBuilder sb = new SuccTacletBuilder();
087: sb.setIfSequent(seq);
088: sb.setFind(t2);
089: try {
090: sb.getTaclet();
091: } catch (IllegalArgumentException e) {
092: thrown = true;
093: }
094: assertTrue(
095: "An exception should be thrown as a bound SchemaVariable "
096: + "occurs more than once in the Taclets if and find",
097: thrown);
098: }
099:
100: public void testUniquenessOfIfAndFindVarSVBothInIf() {
101: boolean thrown = false;
102: SortedSchemaVariable u = (SortedSchemaVariable) TacletForTests
103: .getVariables().lookup(new Name("u"));
104: Term A = tf.createFunctionTerm((Function) TacletForTests
105: .getFunctions().lookup(new Name("A")), NO_SUBTERMS);
106: Term t1 = tf.createQuantifierTerm(Op.ALL, u, A);
107: Term t2 = tf.createQuantifierTerm(Op.EX, u, A);
108: Sequent seq = Sequent
109: .createSuccSequent(Semisequent.EMPTY_SEMISEQUENT
110: .insert(0, new ConstrainedFormula(t1))
111: .semisequent().insert(1,
112: new ConstrainedFormula(t2))
113: .semisequent());
114: SuccTacletBuilder sb = new SuccTacletBuilder();
115: sb.setIfSequent(seq);
116: sb.setFind(A);
117: try {
118: sb.getTaclet();
119: } catch (IllegalArgumentException e) {
120: thrown = true;
121: }
122: assertTrue(
123: "An exception should be thrown as a bound SchemaVariable "
124: + "occurs more than once in the Taclets if and find",
125: thrown);
126: }
127:
128: public void testUniquenessOfIfAndFindVarSVsInFind() {
129: boolean thrown = false;
130: SortedSchemaVariable u = (SortedSchemaVariable) TacletForTests
131: .getVariables().lookup(new Name("u"));
132: Term A = tf.createFunctionTerm((Function) TacletForTests
133: .getFunctions().lookup(new Name("A")), NO_SUBTERMS);
134: Term t1 = tf.createQuantifierTerm(Op.ALL, u, A);
135: SuccTacletBuilder sb = new SuccTacletBuilder();
136: sb.setFind(tf.createJunctorTerm(Op.AND, t1, t1));
137: try {
138: sb.getTaclet();
139: } catch (IllegalArgumentException e) {
140: thrown = true;
141: }
142: assertTrue(
143: "An exception should be thrown as a bound SchemaVariable "
144: + "occurs more than once in the Taclets if and find",
145: thrown);
146: }
147:
148: private final HelperClassForTests helper = new HelperClassForTests();
149:
150: public static final String testRules = System
151: .getProperty("key.home")
152: + File.separator
153: + "examples"
154: + File.separator
155: + "_testcase" + File.separator + "tacletprefix";
156:
157: public void testSchemavariablesInAddrulesRespectPrefix() {
158: try {
159: helper.parseThrowException(new File(testRules
160: + File.separator
161: + "schemaVarInAddruleRespectPrefix.key"));
162: } catch (Throwable t) {
163: assertTrue(
164: "Expected taclet prefix exception but was " + t,
165: t instanceof TacletPrefixBuilder.InvalidPrefixException);
166: return;
167: }
168: fail("Expected an invalid prefix exception as the the addrule contains "
169: + "a schemavariable with wrong prefix.");
170:
171: }
172:
173: }
|