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:
11: package de.uka.ilkd.key.rule.soundness;
12:
13: import org.apache.log4j.Logger;
14:
15: import de.uka.ilkd.key.java.ArrayOfStatement;
16: import de.uka.ilkd.key.java.Services;
17: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
18: import de.uka.ilkd.key.logic.op.ListOfIProgramVariable;
19: import de.uka.ilkd.key.logic.op.SchemaVariable;
20: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
21: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
22:
23: /**
24: * Create statement skolem symbols to instantiate schema variables for
25: * statements
26: */
27: public class StatementSkolemBuilder extends
28: StatementExpressionSkolemBuilder {
29:
30: public StatementSkolemBuilder(SkolemSet p_oriSkolemSet,
31: ProgramVariablePrefixes p_prefixes,
32: JumpStatementPrefixes p_jumpStatementPrefixes,
33: Services p_services) {
34: super (p_oriSkolemSet, p_prefixes, p_jumpStatementPrefixes,
35: p_services);
36: }
37:
38: public IteratorOfSkolemSet build() {
39: IteratorOfSchemaVariable it = getOriginalSkolemSet()
40: .getMissing().iterator();
41:
42: while (it.hasNext()) {
43: final SchemaVariable sv = it.next();
44:
45: if (sv.isProgramSV()
46: && ((SortedSchemaVariable) sv).sort() == ProgramSVSort.STATEMENT
47: && !isInstantiated(sv))
48: createSkolemStatementSV(sv);
49: }
50:
51: return toIterator(getOriginalSkolemSet().add(getSVI())
52: .addVariables(getVariables()).addTaclets(getTaclets()));
53: }
54:
55: private void createSkolemStatementSV(SchemaVariable p_sv) {
56: Logger.getLogger("key.taclet_soundness").debug(
57: "createSkolemStatementSV() with " + p_sv);
58:
59: final StatementSymbolArgBuilder b = new StatementSymbolArgBuilder(
60: p_sv);
61: final ProgramSVProxy proxy = createStatementSymbol(""
62: + p_sv.name(), b.getInfluencingPVs(), b.getJumpTable());
63: addInstantiation(p_sv, proxy);
64: }
65:
66: private ProgramSVProxy createStatementSymbol(String baseName,
67: ListOfIProgramVariable p_pvArgs, ArrayOfStatement jumpTable) {
68: final StatementSkolemSymbolFactory f = new StatementSkolemSymbolFactory(
69: getServices());
70:
71: final ProgramSVProxy proxy = f.createStatementSymbol(
72: createUniquePEName(baseName), p_pvArgs, jumpTable);
73:
74: addVocabulary(f);
75:
76: return proxy;
77: }
78:
79: }
|