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: package de.uka.ilkd.key.java.declaration;
12:
13: import de.uka.ilkd.key.java.abstraction.Type;
14: import de.uka.ilkd.key.java.visitor.Visitor;
15: import de.uka.ilkd.key.logic.op.ProgramVariable;
16:
17: /* An implicit field specification. In KeY we store information about states of
18: * classes and/or objects as static or instance fields
19: * (e.g. if a class is initialized or an object created). To avoid name clashes
20: * the name of implicit fields is enclosed by angle brackets.
21: */
22: public class ImplicitFieldSpecification extends FieldSpecification {
23:
24: /**
25: * Implicit Field specification.
26: */
27: public ImplicitFieldSpecification() {
28: }
29:
30: /**
31: * Implicit Field specification.
32: * @param var the ProgramVariable representing this concrete field
33: */
34: public ImplicitFieldSpecification(ProgramVariable var) {
35: this (var, var.getKeYJavaType());
36: }
37:
38: /**
39: * Implicit Field specification.
40: * @param var the ProgramVariable representing this concrete field
41: * @param type the Type of this field
42: */
43:
44: public ImplicitFieldSpecification(ProgramVariable var, Type type) {
45: super (var, type);
46: }
47:
48: /** calls the corresponding method of a visitor in order to
49: * perform some action/transformation on this element
50: * @param v the Visitor
51: */
52: public void visit(Visitor v) {
53: v.performActionOnImplicitFieldSpecification(this);
54: }
55:
56: }
|