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: package de.uka.ilkd.key.rule.conditions;
009:
010: import java.util.HashSet;
011: import java.util.Iterator;
012: import java.util.LinkedList;
013:
014: import de.uka.ilkd.key.java.Label;
015: import de.uka.ilkd.key.java.ProgramElement;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.visitor.LabelCollector;
018: import de.uka.ilkd.key.logic.op.*;
019: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
020: import de.uka.ilkd.key.rule.MatchConditions;
021: import de.uka.ilkd.key.rule.VariableCondition;
022: import de.uka.ilkd.key.rule.inst.SVInstantiations;
023:
024: /**
025: * This variable condition ensures that no other label of the
026: * same name exists in the context program or one of the schemavariable
027: * instantiations.
028: */
029: public class NewJumpLabelCondition implements VariableCondition {
030:
031: private final ProgramSV labelSV;
032:
033: public NewJumpLabelCondition(SchemaVariable sv) {
034:
035: if (!(sv instanceof ProgramSV)
036: || ((ProgramSV) sv).sort() != ProgramSVSort.LABEL) {
037: throw new IllegalArgumentException(
038: "The new jump label "
039: + "variable condition, must be parameterised with a "
040: + "program schemavariable of sort LABEL.");
041: }
042:
043: labelSV = (ProgramSV) sv;
044: }
045:
046: public MatchConditions check(SchemaVariable var,
047: SVSubstitute instCandidate, MatchConditions matchCond,
048: Services services) {
049: if (var != labelSV
050: && matchCond.getInstantiations()
051: .isInstantiated(labelSV)) {
052: var = labelSV;
053: instCandidate = (SVSubstitute) matchCond
054: .getInstantiations().getInstantiation(labelSV);
055: }
056:
057: if (var == labelSV) {
058: if (!(instCandidate instanceof Label)) {
059: return null;
060: }
061: final LinkedList programs = collect(matchCond
062: .getInstantiations());
063: programs.add(matchCond.getInstantiations()
064: .getContextInstantiation().contextProgram());
065: if (!isUnique((Label) instCandidate, programs)) {
066: return null;
067: }
068: }
069: return matchCond;
070: }
071:
072: private LinkedList collect(SVInstantiations inst) {
073: final LinkedList result = new LinkedList();
074: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = inst
075: .pairIterator();
076: while (it.hasNext()) {
077: final EntryOfSchemaVariableAndInstantiationEntry entry = it
078: .next();
079: if (entry.key() != labelSV
080: && entry.value() != null
081: && entry.value().getInstantiation() instanceof ProgramElement) {
082: result.add(entry.value().getInstantiation());
083: }
084: }
085: return result;
086: }
087:
088: private boolean isUnique(Label label, LinkedList programs) {
089: final HashSet result = new HashSet(100);
090: for (final Iterator it = programs.iterator(); it.hasNext();) {
091: final LabelCollector lc = new LabelCollector(
092: (ProgramElement) it.next(), result);
093: lc.start();
094: }
095: return !result.contains(label);
096: }
097:
098: public String toString() {
099: return "\\newLabel (" + labelSV + ")";
100: }
101: }
|