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: /**
12: * container for the application part of an Taclet. It contains an
13: * if-sequence, a list of new variables and a list of variable pairs
14: * inidcating the NotFreeIn relation and a list of program variables to
15: * be added to the program context.
16: */package de.uka.ilkd.key.rule;
17:
18: import de.uka.ilkd.key.logic.Sequent;
19:
20: public class TacletApplPart {
21:
22: private Sequent ifseq;
23: private ListOfNewVarcond varsNew;
24: private ListOfNotFreeIn varsNotFreeIn;
25: private ListOfNewDependingOn varsNewDependingOn;
26: private ListOfVariableCondition variableConditions;
27:
28: /** constructs a new TacletApplPart object with the given Sequent,
29: * a list of variables that are new, a list of variable pairs that
30: * represent the NotFreeIn relation and a list of additional
31: * generic variable conditions.
32: */
33: public TacletApplPart(Sequent ifseq, ListOfNewVarcond varsNew,
34: ListOfNotFreeIn varsNotFreeIn,
35: ListOfNewDependingOn varsNewDependingOn,
36: ListOfVariableCondition variableConditions) {
37: this .ifseq = ifseq;
38: this .varsNew = varsNew;
39: this .varsNotFreeIn = varsNotFreeIn;
40: this .varsNewDependingOn = varsNewDependingOn;
41: this .variableConditions = variableConditions;
42: }
43:
44: /** returns the if-sequent of the application part of a Taclet */
45: public Sequent ifSequent() {
46: return ifseq;
47: }
48:
49: /** returns the list of variables that are new in a Taclet */
50: public ListOfNewVarcond varsNew() {
51: return varsNew;
52: }
53:
54: /** returns the list of variable pairs that represent the
55: * NotFreeIn relation of a Taclet
56: */
57: public ListOfNotFreeIn varsNotFreeIn() {
58: return varsNotFreeIn;
59: }
60:
61: /** returns the list of variable pairs that represent the
62: * "new depending on" relation of a Taclet
63: */
64: public ListOfNewDependingOn varsNewDependingOn() {
65: return varsNewDependingOn;
66: }
67:
68: /** returns the list of additional generic conditions on
69: * instantiations of schema variables. The list ist readonly. */
70: public ListOfVariableCondition getVariableConditions() {
71: return variableConditions;
72: }
73:
74: }
|