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 de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.ProgramElementName;
15: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
16: import de.uka.ilkd.key.logic.op.SchemaVariable;
17: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
18: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
19:
20: /**
21: * Create skolem symbols (labels) for schema variables for labels.
22: */
23: public class LabelSkolemBuilder extends AbstractSkolemBuilder {
24:
25: public LabelSkolemBuilder(SkolemSet p_oriSkolemSet,
26: Services p_services) {
27: super (p_oriSkolemSet, p_services);
28: }
29:
30: public IteratorOfSkolemSet build() {
31: IteratorOfSchemaVariable it = getOriginalSkolemSet()
32: .getMissing().iterator();
33: SchemaVariable sv;
34:
35: while (it.hasNext()) {
36: sv = it.next();
37:
38: if (sv.isProgramSV()
39: && ((SortedSchemaVariable) sv).sort() == ProgramSVSort.LABEL)
40: createSkolemLabel(sv);
41: }
42:
43: return toIterator(getOriginalSkolemSet().add(getSVI()));
44: }
45:
46: private void createSkolemLabel(SchemaVariable p_sv) {
47: if (!isInstantiated(p_sv)) {
48: ProgramElementName name = createUniquePEName(p_sv.name());
49: addInstantiation(p_sv, name);
50: }
51:
52: }
53:
54: }
|