01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10: package de.uka.ilkd.key.java;
11:
12: import junit.framework.TestCase;
13: import de.uka.ilkd.key.java.expression.literal.StringLiteral;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.rule.TacletForTests;
16:
17: public class TestTypeConverter extends TestCase {
18:
19: static String[][] stringTests = {
20: {
21: "\"test\"",
22: "cat(Z(6(1(1(#)))),cat(Z(1(0(1(#)))),cat(Z(5(1(1(#)))),cat(Z(6(1(1(#)))),epsilon))))" },
23: { "\"\"", "epsilon" } };
24:
25: private Services serv;
26: private TypeConverter tc;
27:
28: public TestTypeConverter(String name) {
29: super (name);
30: }
31:
32: public void setUp() {
33: TacletForTests.parse();
34: serv = TacletForTests.services();
35: serv.setNamespaces(TacletForTests.getNamespaces());
36: tc = serv.getTypeConverter();
37: }
38:
39: public void tearDown() {
40: serv = null;
41: tc = null;
42: }
43:
44: public void testStringConverter() {
45: Term t, match;
46: for (int i = 0; i < stringTests.length; i++) {
47: t = tc.convertToLogicElement(new StringLiteral(
48: stringTests[i][0]));
49: match = TacletForTests.parseTerm(stringTests[i][1], serv
50: .getNamespaces());
51: assertTrue("Expected that StringLiteral "
52: + stringTests[i][0] + " is translated to "
53: + stringTests[i][1], match.equals(t));
54:
55: Expression stringExpr = TypeConverter.stringConverter
56: .translateTerm(match, null);
57: assertTrue("Expected that Term " + stringTests[i][1]
58: + " is translated to " + stringTests[i][0],
59: stringExpr.equals(new StringLiteral(
60: stringTests[i][0])));
61: }
62: }
63:
64: }
|