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.proof.mgt;
09:
10: import de.uka.ilkd.key.logic.Term;
11: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
12: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
13:
14: /**
15: * represents an update pair (lhs, rhs) with a guard and quantified
16: * variables <code>v1,...,vn</code>, which would be written as
17: * <code>\for v1,...,vn \if guard lhs := rhs</code>
18: */
19: public class UpdatePairWithGuard {
20: private Term lhs;
21: private Term rhs;
22: Term guard;
23: private QuantifiableVariable[] qvars;
24:
25: public UpdatePairWithGuard(Term lhs, Term rhs, Term guard,
26: QuantifiableVariable[] qvars) {
27: this .lhs = lhs;
28: this .rhs = rhs;
29: this .guard = guard;
30: this .qvars = qvars;
31: }
32:
33: public Term getLHS() {
34: return lhs;
35: }
36:
37: public Term getRHS() {
38: return rhs;
39: }
40:
41: public Term getGuard() {
42: return guard;
43: }
44:
45: public QuantifiableVariable[] getQuantifiedVars() {
46: return qvars;
47: }
48:
49: public ArrayOfQuantifiableVariable createArrayOfQuantifiedVars() {
50: return new ArrayOfQuantifiableVariable(qvars);
51: }
52: }
|