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.ArrayOfStatement;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.logic.ProgramElementName;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
019: import de.uka.ilkd.key.rule.inst.ProgramSkolemInstantiation;
020:
021: /**
022: * Create expression skolem symbols to instantiate schema variables for
023: * expressions
024: */
025: public class ExpressionSkolemBuilder extends
026: StatementExpressionSkolemBuilder {
027:
028: public ExpressionSkolemBuilder(SkolemSet p_oriSkolemSet,
029: ProgramVariablePrefixes p_prefixes,
030: JumpStatementPrefixes p_jumpStatementPrefixes,
031: Services p_services) {
032: super (p_oriSkolemSet, p_prefixes, p_jumpStatementPrefixes,
033: p_services);
034: }
035:
036: public IteratorOfSkolemSet build() {
037: ListOfSchemaVariable todo = findExpressionSVs(getOriginalSkolemSet());
038:
039: return createSkolemExpressionSVs(todo);
040: }
041:
042: public static ListOfSchemaVariable findExpressionSVs(SkolemSet p_ss) {
043: IteratorOfSchemaVariable it = p_ss.getMissing().iterator();
044: SchemaVariable sv;
045: ListOfSchemaVariable res = SLListOfSchemaVariable.EMPTY_LIST;
046:
047: while (it.hasNext()) {
048: sv = it.next();
049:
050: if (sv.isProgramSV()
051: && ((SortedSchemaVariable) sv).sort() == ProgramSVSort.EXPRESSION)
052: res = res.prepend(sv);
053: }
054:
055: return res;
056: }
057:
058: private IteratorOfSkolemSet createSkolemExpressionSVs(
059: ListOfSchemaVariable p_svs) {
060: IteratorOfSchemaVariable it = p_svs.iterator();
061: while (it.hasNext())
062: createSkolemExpressionSV(it.next());
063:
064: return toIterator(getOriginalSkolemSet().add(getSVI())
065: .addVariables(getVariables()).addTaclets(getTaclets()));
066: }
067:
068: private void createSkolemExpressionSV(SchemaVariable p_sv) {
069: final SVTypeInfo svti = getOriginalSkolemSet().getSVTypeInfos()
070: .getInfo(p_sv);
071:
072: createSkolemExpressionSV(p_sv, svti.getType());
073: }
074:
075: private void createSkolemExpressionSV(SchemaVariable p_sv,
076: KeYJavaType p_type) {
077: final String baseName = "" + p_sv.name() + "_"
078: + p_type.getJavaType().getFullName();
079: ProgramElementName name = createUniquePEName(baseName);
080: final StatementSymbolArgBuilder b = new StatementSymbolArgBuilder(
081: p_sv);
082:
083: final ProgramSVProxy proxy = createSkolemExpressionSV(name,
084: p_type, b.getInfluencingPVs(), b.getJumpTable());
085:
086: addInstantiation(p_sv, proxy,
087: ProgramSkolemInstantiation.NEW_EXPRESSION);
088: }
089:
090: private ProgramSVProxy createSkolemExpressionSV(
091: ProgramElementName p_name, KeYJavaType p_type,
092: ListOfIProgramVariable p_influencingPVs,
093: ArrayOfStatement p_jumpTable) {
094: final ExpressionSkolemSymbolFactory f = new ExpressionSkolemSymbolFactory(
095: getServices());
096:
097: final ProgramSVProxy proxy = f.createExpressionSymbol(p_name,
098: p_type, p_influencingPVs, p_jumpTable);
099:
100: addVocabulary(f);
101:
102: return proxy;
103: }
104:
105: }
|