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: package de.uka.ilkd.key.rule.conditions;
09:
10: import de.uka.ilkd.key.java.Services;
11: import de.uka.ilkd.key.logic.op.SVSubstitute;
12: import de.uka.ilkd.key.logic.op.SchemaVariable;
13: import de.uka.ilkd.key.rule.MatchConditions;
14: import de.uka.ilkd.key.rule.VariableCondition;
15:
16: public class NewDepOnAnonUpdates implements VariableCondition {
17:
18: private final SchemaVariable modifiesSV, updateSV;
19:
20: public NewDepOnAnonUpdates(SchemaVariable update,
21: SchemaVariable modifies) {
22: this .modifiesSV = modifies;
23: this .updateSV = update;
24: assert updateSV.isFormulaSV() : "newDependingOnMod: First argument has to be a formulaSV";
25: assert modifies.isListSV() : "newDependingOnMod: Second argument has to be a listSV";
26: }
27:
28: public MatchConditions check(SchemaVariable var,
29: SVSubstitute instCandidate, MatchConditions matchCond,
30: Services services) {
31:
32: return matchCond;
33: }
34:
35: public String toString() {
36: return "\\new(" + updateSV + ", \\dependingOnMod(" + modifiesSV
37: + ")";
38: }
39:
40: public SchemaVariable getModifiesSV() {
41: return modifiesSV;
42: }
43:
44: public SchemaVariable getUpdateSV() {
45: return updateSV;
46: }
47: }
|