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.JavaInfo;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.abstraction.*;
016: import de.uka.ilkd.key.logic.*;
017: import de.uka.ilkd.key.logic.op.*;
018:
019: /**
020: * Factory for the four kinds of skolem symbols
021: * (for terms, formulas, statements and expressions)
022: */
023: abstract class SkolemSymbolFactory {
024:
025: private final Services services;
026:
027: private final Namespace functions = new Namespace();
028: private final Namespace variables = new Namespace();
029:
030: SkolemSymbolFactory(Services p_services) {
031: super ();
032: services = p_services;
033: }
034:
035: protected void addVariable(Named p) {
036: variables.add(p);
037: }
038:
039: protected void addFunction(Named p) {
040: functions.add(p);
041: }
042:
043: protected void addVocabulary(SkolemSymbolFactory p) {
044: variables.add(p.variables);
045: }
046:
047: protected ArrayOfIProgramVariable getProgramVariablesAsArray(
048: ListOfIProgramVariable p) {
049:
050: int pvpSize = p.size();
051:
052: IProgramVariable[] pva = new IProgramVariable[pvpSize];
053:
054: IteratorOfIProgramVariable it = p.iterator();
055:
056: int i = 0;
057: while (it.hasNext()) {
058: pva[i] = it.next();
059: ++i;
060: }
061:
062: return new ArrayOfIProgramVariable(pva);
063: }
064:
065: protected ArrayOfKeYJavaType getKeYJavaTypesAsArray(
066: ListOfKeYJavaType p) {
067:
068: int pvpSize = p.size();
069:
070: KeYJavaType[] pva = new KeYJavaType[pvpSize];
071:
072: IteratorOfKeYJavaType it = p.iterator();
073:
074: int i = 0;
075: while (it.hasNext()) {
076: pva[i] = it.next();
077: ++i;
078: }
079:
080: return new ArrayOfKeYJavaType(pva);
081: }
082:
083: public ListOfIProgramVariable getProgramVariablesAsList(
084: ArrayOfIProgramVariable p) {
085:
086: ListOfIProgramVariable res = SLListOfIProgramVariable.EMPTY_LIST;
087:
088: int i = p.size();
089: while (i-- != 0)
090: res = res.prepend(p.getIProgramVariable(i));
091:
092: return res;
093:
094: }
095:
096: protected ListOfKeYJavaType getKeYJavaTypesAsList(
097: ArrayOfKeYJavaType p) {
098:
099: ListOfKeYJavaType res = SLListOfKeYJavaType.EMPTY_LIST;
100:
101: int i = p.size();
102: while (i-- != 0)
103: res = res.prepend(p.getKeYJavaType(i));
104:
105: return res;
106:
107: }
108:
109: protected ArrayOfKeYJavaType getProgramVariableTypes(
110: ListOfIProgramVariable p) {
111:
112: int pvpSize = p.size();
113:
114: KeYJavaType[] types = new KeYJavaType[pvpSize];
115: IteratorOfIProgramVariable it = p.iterator();
116:
117: int i = 0;
118: while (it.hasNext()) {
119: types[i] = it.next().getKeYJavaType();
120: ++i;
121: }
122:
123: return new ArrayOfKeYJavaType(types);
124:
125: }
126:
127: protected TermFactory getTF() {
128: return TermFactory.DEFAULT;
129: }
130:
131: protected Services getServices() {
132: return services;
133: }
134:
135: protected JavaInfo getJavaInfo() {
136: return getServices().getJavaInfo();
137: }
138:
139: /**
140: * HACK: Create a new and unique identifier
141: */
142: protected static Name createUniqueName(String baseName) {
143: return AbstractSkolemBuilder.createUniqueName(baseName);
144: }
145:
146: /**
147: * HACK: Create a new and unique identifier
148: */
149: protected static Name createUniqueName(Name baseName) {
150: return AbstractSkolemBuilder.createUniqueName(baseName);
151: }
152:
153: /**
154: * HACK: Create a new and unique identifier
155: */
156: protected static ProgramElementName createUniquePEName(
157: String baseName) {
158: return AbstractSkolemBuilder.createUniquePEName(baseName);
159: }
160:
161: /**
162: * HACK: Create a new and unique identifier
163: */
164: protected static ProgramElementName createUniquePEName(Name baseName) {
165: return AbstractSkolemBuilder.createUniquePEName(baseName);
166: }
167:
168: /**
169: * @return a namespace of all variables (i.e. program variables)
170: * that have been created as part of the skolem symbol construction
171: */
172: public Namespace getVariables() {
173: return variables;
174: }
175:
176: /**
177: * @return a namespace of all function symbols
178: * that have been created as part of the skolem symbol construction
179: */
180: public Namespace getFunctions() {
181: return functions;
182: }
183:
184: }
|