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.*;
015: import de.uka.ilkd.key.logic.op.*;
016:
017: public abstract class AbstractPVPrefixSkolemBuilder extends
018: AbstractSkolemBuilder {
019:
020: private final ProgramVariablePrefixes prefixes;
021:
022: public AbstractPVPrefixSkolemBuilder(SkolemSet p_oriSkolemSet,
023: ProgramVariablePrefixes p_prefixes, Services p_services) {
024: super (p_oriSkolemSet, p_services);
025: prefixes = p_prefixes;
026: }
027:
028: protected ProgramVariablePrefixes getProgramVariablePrefixes() {
029: return prefixes;
030: }
031:
032: protected ListOfIProgramVariable getProgramVariablePrefix(
033: SchemaVariable p) {
034: ListOfIProgramVariable res = getProgramVariablePrefixes()
035: .getPrefix(p);
036: if (res == null)
037: res = SLListOfIProgramVariable.EMPTY_LIST;
038: return res;
039: }
040:
041: protected ArrayOfIProgramVariable getProgramVariablePrefixAsArray(
042: SchemaVariable p) {
043: return getProgramVariablesAsArray(getProgramVariablePrefix(p));
044: }
045:
046: protected ArrayOfIProgramVariable getProgramVariablesAsArray(
047: ListOfIProgramVariable p) {
048:
049: int pvpSize = p.size();
050:
051: IProgramVariable[] pva = new IProgramVariable[pvpSize];
052:
053: IteratorOfIProgramVariable it = p.iterator();
054:
055: int i = 0;
056: while (it.hasNext()) {
057: pva[i] = it.next();
058: ++i;
059: }
060:
061: return new ArrayOfIProgramVariable(pva);
062: }
063:
064: protected ArrayOfKeYJavaType getKeYJavaTypesAsArray(
065: ListOfKeYJavaType p) {
066:
067: int pvpSize = p.size();
068:
069: KeYJavaType[] pva = new KeYJavaType[pvpSize];
070:
071: IteratorOfKeYJavaType it = p.iterator();
072:
073: int i = 0;
074: while (it.hasNext()) {
075: pva[i] = it.next();
076: ++i;
077: }
078:
079: return new ArrayOfKeYJavaType(pva);
080: }
081:
082: public ListOfIProgramVariable getProgramVariablesAsList(
083: ArrayOfIProgramVariable p) {
084:
085: ListOfIProgramVariable res = SLListOfIProgramVariable.EMPTY_LIST;
086:
087: int i = p.size();
088: while (i-- != 0)
089: res = res.prepend(p.getIProgramVariable(i));
090:
091: return res;
092:
093: }
094:
095: protected ListOfKeYJavaType getKeYJavaTypesAsList(
096: ArrayOfKeYJavaType p) {
097:
098: ListOfKeYJavaType res = SLListOfKeYJavaType.EMPTY_LIST;
099:
100: int i = p.size();
101: while (i-- != 0)
102: res = res.prepend(p.getKeYJavaType(i));
103:
104: return res;
105:
106: }
107:
108: protected ArrayOfKeYJavaType getProgramVariablePrefixTypes(
109: SchemaVariable p) {
110: return getProgramVariableTypes(getProgramVariablePrefix(p));
111: }
112:
113: protected ArrayOfKeYJavaType getProgramVariableTypes(
114: ListOfIProgramVariable p) {
115:
116: int pvpSize = p.size();
117:
118: KeYJavaType[] types = new KeYJavaType[pvpSize];
119: IteratorOfIProgramVariable it = p.iterator();
120:
121: int i = 0;
122: while (it.hasNext()) {
123: types[i] = it.next().getKeYJavaType();
124: ++i;
125: }
126:
127: return new ArrayOfKeYJavaType(types);
128:
129: }
130:
131: }
|