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.soundness;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.logic.JavaBlock;
016: import de.uka.ilkd.key.logic.Name;
017: import de.uka.ilkd.key.logic.Sequent;
018: import de.uka.ilkd.key.logic.Term;
019: import de.uka.ilkd.key.logic.op.*;
020: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
021: import de.uka.ilkd.key.rule.*;
022:
023: /**
024: * This class provides methods that are used to construct taclets
025: * (which are needed to create skolem symbols for statements and
026: * expressions)
027: */
028: abstract class SkolemSymbolTacletFactory extends SkolemSymbolFactory {
029:
030: private ListOfTacletApp taclets = SLListOfTacletApp.EMPTY_LIST;
031:
032: SkolemSymbolTacletFactory(Services p_services) {
033: super (p_services);
034: }
035:
036: /**
037: * @return all created taclets
038: */
039: public ListOfTacletApp getTaclets() {
040: return taclets;
041: }
042:
043: /**
044: * Create rewrite taclets that split a Java block in two separate
045: * (nested) blocks
046: * @param p_find the block to rewrite
047: * @param p_replace the inner replacement block
048: * @param p_sep the outer replacement block
049: * @param p_name base name of the taclets
050: */
051: protected void createTaclets(JavaBlock p_find, JavaBlock p_replace,
052: JavaBlock p_sep, String p_name) {
053: createBoxTaclet(p_find, p_replace, p_sep, p_name);
054: createDiamondTaclet(p_find, p_replace, p_sep, p_name);
055: }
056:
057: private void createBoxTaclet(JavaBlock p_find, JavaBlock p_replace,
058: JavaBlock p_sep, String p_name) {
059: SchemaVariable post = SchemaVariableFactory.createFormulaSV(
060: new Name("post"), false);
061: Term find = getTF().createBoxTerm(p_find,
062: getTF().createVariableTerm(post));
063: Term rw = getTF().createBoxTerm(
064: p_sep,
065: getTF().createBoxTerm(p_replace,
066: getTF().createVariableTerm(post)));
067:
068: createTaclet(find, rw, p_name + "_box");
069: }
070:
071: private void createDiamondTaclet(JavaBlock p_find,
072: JavaBlock p_replace, JavaBlock p_sep, String p_name) {
073: SchemaVariable post = SchemaVariableFactory.createFormulaSV(
074: new Name("post"), false);
075: Term find = getTF().createDiamondTerm(p_find,
076: getTF().createVariableTerm(post));
077: Term rw = getTF().createDiamondTerm(
078: p_sep,
079: getTF().createDiamondTerm(p_replace,
080: getTF().createVariableTerm(post)));
081:
082: createTaclet(find, rw, p_name + "_dia");
083: }
084:
085: /**
086: * Create taclets that rewrite a Java block
087: * @param p_find the block to rewrite
088: * @param p_replace the new block
089: * @param p_name base name of the taclets
090: */
091: protected void createTaclets(JavaBlock p_find, JavaBlock p_replace,
092: String p_name) {
093: createBoxTaclet(p_find, p_replace, p_name);
094: createDiamondTaclet(p_find, p_replace, p_name);
095: }
096:
097: private void createBoxTaclet(JavaBlock p_find, JavaBlock p_replace,
098: String p_name) {
099: SchemaVariable post = SchemaVariableFactory.createFormulaSV(
100: new Name("post"), false);
101: Term find = getTF().createBoxTerm(p_find,
102: getTF().createVariableTerm(post));
103: Term rw = getTF().createBoxTerm(p_replace,
104: getTF().createVariableTerm(post));
105:
106: createTaclet(find, rw, p_name + "_box");
107: }
108:
109: private void createDiamondTaclet(JavaBlock p_find,
110: JavaBlock p_replace, String p_name) {
111: SchemaVariable post = SchemaVariableFactory.createFormulaSV(
112: new Name("post"), false);
113: Term find = getTF().createDiamondTerm(p_find,
114: getTF().createVariableTerm(post));
115: Term rw = getTF().createDiamondTerm(p_replace,
116: getTF().createVariableTerm(post));
117:
118: createTaclet(find, rw, p_name + "_dia");
119: }
120:
121: private void createTaclet(Term p_find, Term p_rw, String p_name) {
122: RewriteTacletBuilder builder = new RewriteTacletBuilder();
123:
124: builder.setFind(p_find);
125:
126: RewriteTacletGoalTemplate goal = new RewriteTacletGoalTemplate(
127: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST, p_rw);
128: builder.addTacletGoalTemplate(goal);
129:
130: builder.setName(new Name(p_name));
131:
132: taclets = taclets.prepend(NoPosTacletApp
133: .createNoPosTacletApp(builder.getTaclet()));
134: }
135:
136: /**
137: * Create an array of PVSV which is compatible to the
138: * program variable arguments of <code>p</code>
139: */
140: protected ArrayOfIProgramVariable createSVsForInfluencingPVs(
141: ProgramSVProxy p) {
142:
143: int i = p.getInfluencingPVs().size();
144: IProgramVariable[] res = new IProgramVariable[i];
145:
146: while (i-- != 0)
147: res[i] = (IProgramVariable) SchemaVariableFactory
148: .createProgramSV(createUniquePEName("pv"),
149: ProgramSVSort.VARIABLE, false);
150:
151: return new ArrayOfIProgramVariable(res);
152: }
153:
154: protected void addVocabulary(SkolemSymbolFactory p) {
155: super .addVocabulary(p);
156: if (p instanceof SkolemSymbolTacletFactory)
157: taclets = taclets
158: .prepend(((SkolemSymbolTacletFactory) p).taclets);
159: }
160:
161: protected ProgramVariable createSelectorVariable() {
162: final ProgramVariable sel = new LocationVariable(
163: createUniquePEName("sel"), getSelectorType());
164: addVariable(sel);
165: return sel;
166: }
167:
168: protected KeYJavaType getSelectorType() {
169: return getJavaInfo().getPrimitiveKeYJavaType("int");
170: }
171:
172: }
|