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-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016: //
017: //
018:
019: package de.uka.ilkd.key.logic;
020:
021: import junit.framework.TestCase;
022: import de.uka.ilkd.key.java.Services;
023: import de.uka.ilkd.key.java.Statement;
024: import de.uka.ilkd.key.java.StatementBlock;
025: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
026: import de.uka.ilkd.key.java.expression.operator.PostIncrement;
027: import de.uka.ilkd.key.logic.op.*;
028: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
029: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
030: import de.uka.ilkd.key.proof.*;
031: import de.uka.ilkd.key.rule.*;
032: import de.uka.ilkd.key.rule.inst.SVInstantiations;
033:
034: public class TestVariableNamer extends TestCase {
035:
036: private final Services services = new Services();
037: private final Proof proof = new Proof(services);
038: private final ProgramVariable x = constructProgramVariable("x");
039: private final ProgramVariable xx = constructProgramVariable("x");
040: private final ProgramVariable y = constructProgramVariable("y");
041: private final ProgramVariable x_1 = constructProgramVariable("x_1");
042: private final ProgramVariable x_2 = constructProgramVariable("x_2");
043: private final ProgramVariable var_1 = constructProgramVariable("var_1");
044: private final ProgramVariable var_2 = constructProgramVariable("var_2");
045: private final ConstrainedFormula formulaWithX = constructFormula(x);
046: private final ConstrainedFormula formulaWithX_1 = constructFormula(x_1);
047: private final ConstrainedFormula formulaWithVar_1 = constructFormula(var_1);
048: private final SortedSchemaVariable variableSV = (SortedSchemaVariable) SchemaVariableFactory
049: .createProgramSV(new ProgramElementName("sv"),
050: ProgramSVSort.VARIABLE, false);
051:
052: public TestVariableNamer(String name) {
053: super (name);
054: }
055:
056: private ProgramVariable constructProgramVariable(
057: ProgramElementName name) {
058: KeYJavaType myKeyJavaType = new KeYJavaType(new PrimitiveSort(
059: new Name("mysort")));
060: return new LocationVariable(name, myKeyJavaType);
061: }
062:
063: private ProgramVariable constructProgramVariable(String name) {
064: ProgramElementName pen = VariableNamer.parseName(name);
065: assertTrue(pen.toString().equals(name));
066: return constructProgramVariable(pen);
067: }
068:
069: private ConstrainedFormula constructFormula(
070: ProgramVariable containedVar) {
071: Statement statement = new PostIncrement(containedVar);
072: StatementBlock statementBlock = new StatementBlock(statement);
073: JavaBlock javaBlock = JavaBlock.createJavaBlock(statementBlock);
074:
075: TermFactory termFactory = TermFactory.DEFAULT;
076: Term subterm = termFactory.createJunctorTerm(Op.TRUE);
077: Term term = termFactory.createDiamondTerm(javaBlock, subterm);
078:
079: return new ConstrainedFormula(term);
080: }
081:
082: private PosInOccurrence constructPIO(ConstrainedFormula formula) {
083: return new PosInOccurrence(formula, PosInTerm.TOP_LEVEL, true);
084: }
085:
086: private Goal constructGoal(ConstrainedFormula containedFormula) {
087: Semisequent empty = Semisequent.EMPTY_SEMISEQUENT;
088: Semisequent ante = empty.insert(0, containedFormula)
089: .semisequent();
090: Semisequent succ = empty;
091:
092: Sequent seq = Sequent.createSequent(ante, succ);
093: Node node = new Node(proof, seq);
094:
095: TacletIndex tacletIndex = new TacletIndex();
096: BuiltInRuleAppIndex builtInRuleAppIndex = new BuiltInRuleAppIndex(
097: new BuiltInRuleIndex());
098: RuleAppIndex ruleAppIndex = new RuleAppIndex(tacletIndex,
099: builtInRuleAppIndex);
100:
101: return new Goal(node, ruleAppIndex);
102: }
103:
104: private void addGlobal(Goal goal, ProgramVariable globalVar) {
105: SetOfProgramVariable globals = goal.getGlobalProgVars().add(
106: globalVar);
107: goal.setGlobalProgVars(globals);
108: }
109:
110: private boolean inGlobals(Goal goal, ProgramVariable globalVar) {
111: IteratorOfProgramVariable it = goal.getGlobalProgVars()
112: .iterator();
113: while (it.hasNext()) {
114: if (it.next() == globalVar) {
115: return true;
116: }
117: }
118: return false;
119: }
120:
121: private void addTacletApp(Goal goal, ProgramVariable containedVar) {
122: Term findTerm = TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
123: AntecTacletBuilder builder = new AntecTacletBuilder();
124: builder.setFind(findTerm);
125: AntecTaclet taclet = builder.getAntecTaclet();
126: NoPosTacletApp app = NoPosTacletApp
127: .createNoPosTacletApp(taclet);
128:
129: SchemaVariable sv = SchemaVariableFactory.createProgramSV(
130: new ProgramElementName("sv"), ProgramSVSort.STATEMENT,
131: false);
132: Statement statement = new PostIncrement(containedVar);
133: app = (NoPosTacletApp) app.addCheckedInstantiation(sv,
134: statement, goal.proof().getServices(), false);
135:
136: goal.ruleAppIndex().tacletIndex().add(app);
137: }
138:
139: private boolean inTacletApps(Goal goal, ProgramVariable containedVar) {
140: RuleAppIndex ruleAppIndex = goal.ruleAppIndex();
141: TacletIndex tacletIndex = ruleAppIndex.tacletIndex();
142: ListOfNoPosTacletApp noPosTacletApps = tacletIndex
143: .getPartialInstantiatedApps();
144:
145: IteratorOfNoPosTacletApp it = noPosTacletApps.iterator();
146: while (it.hasNext()) {
147: SVInstantiations insts = it.next().instantiations();
148: IteratorOfEntryOfSchemaVariableAndInstantiationEntry it2;
149: it2 = insts.pairIterator();
150: while (it2.hasNext()) {
151: EntryOfSchemaVariableAndInstantiationEntry e = it2
152: .next();
153: Object inst = e.value().getInstantiation();
154: if (inst instanceof PostIncrement
155: && ((PostIncrement) inst).getFirstElement() == containedVar) {
156: return true;
157: }
158: }
159: }
160:
161: return false;
162: }
163:
164: public void setUp() {
165: UpdateSimplifier sus = new UpdateSimplifier();
166: proof.setSimplifier(sus);
167: }
168:
169: private void testTemporaryNames(VariableNamer vn) {
170: ProgramElementName name = vn.getTemporaryNameProposal("x");
171: assertFalse(name.getProgramName().equals("x"));
172:
173: ProgramVariable v = constructProgramVariable(name);
174: ConstrainedFormula formula = constructFormula(v);
175: Goal goal = constructGoal(formula);
176: PosInOccurrence pio = constructPIO(formula);
177: v = vn.rename(v, goal, pio);
178: assertTrue(v.getProgramElementName().getProgramName().equals(
179: "x"));
180: }
181:
182: public void testInnerRename() {
183: VariableNamer vn = services.getVariableNamer();
184: ProgramVariable v, w;
185:
186: PosInOccurrence pio = constructPIO(formulaWithX);
187: Goal goal = constructGoal(formulaWithX);
188: Sequent originalSequent = goal.sequent();
189:
190: v = vn.rename(y, goal, pio);
191: assertTrue(v.getProgramElementName().getProgramName().equals(
192: "y"));
193: assertTrue(goal.sequent().equals(originalSequent));
194:
195: v = vn.rename(xx, goal, pio);
196: assertTrue(v.getProgramElementName().getProgramName().equals(
197: "x"));
198: assertTrue(goal.sequent().equals(originalSequent));
199:
200: addGlobal(goal, v);
201: w = vn.rename(x, goal, pio);
202: assertFalse(w.getProgramElementName().getProgramName().equals(
203: "x"));
204: assertFalse(goal.sequent().equals(originalSequent));
205: assertTrue(inGlobals(goal, v));
206:
207: testTemporaryNames(vn);
208: }
209:
210: public void testInnerRenameInTacletApps() {
211: VariableNamer vn = services.getVariableNamer();
212: ProgramVariable v;
213:
214: PosInOccurrence pio = constructPIO(formulaWithX);
215: Goal goal = constructGoal(formulaWithX);
216: addGlobal(goal, xx);
217: addTacletApp(goal, x);
218:
219: v = vn.rename(x, goal, pio);
220: assertFalse(inTacletApps(goal, x));
221: assertTrue(inTacletApps(goal, v));
222: }
223:
224: public void testNameProposals() {
225: VariableNamer vn = services.getVariableNamer();
226: ProgramElementName proposal;
227:
228: PosInOccurrence pio = constructPIO(formulaWithVar_1);
229: Goal goal = constructGoal(formulaWithVar_1);
230:
231: proposal = vn.getNameProposalForSchemaVariable(null,
232: variableSV, pio, null, null);
233: assertTrue(proposal.toString().equals("var_2"));
234:
235: addGlobal(goal, var_2);
236:
237: proposal = vn.getNameProposalForSchemaVariable("var",
238: variableSV, pio, null, null);
239: assertTrue(proposal.toString().equals("var_2"));
240: }
241:
242: public void testInnerRenameUniqueness() {
243: VariableNamer vn = services.getVariableNamer();
244: ProgramVariable v;
245:
246: PosInOccurrence pio = constructPIO(formulaWithX_1);
247: Goal goal = constructGoal(formulaWithX_1);
248: addGlobal(goal, xx);
249: addTacletApp(goal, x_2);
250:
251: v = vn.rename(x, goal, pio);
252: assertTrue(v.getProgramElementName().getProgramName().equals(
253: "x_2"));
254: }
255:
256: }
|