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: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
11: // and Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16:
17: package de.uka.ilkd.key.jml;
18:
19: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
20: import de.uka.ilkd.key.logic.Term;
21: import de.uka.ilkd.key.logic.op.ProgramVariable;
22:
23: /**
24: * Provides an encapsulation for a single signals clause.
25: */
26: public class Signals {
27:
28: private final KeYJavaType kjt;
29: private final ProgramVariable v;
30: private final Term cond;
31:
32: public Signals(KeYJavaType kjt, ProgramVariable v, Term cond) {
33: this .kjt = kjt;
34: this .v = v;
35: this .cond = cond;
36: }
37:
38: public KeYJavaType type() {
39: return kjt;
40: }
41:
42: public ProgramVariable variable() {
43: return v;
44: }
45:
46: public Term condition() {
47: return cond;
48: }
49: }
|