001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java.declaration;
012:
013: import de.uka.ilkd.key.java.Expression;
014: import de.uka.ilkd.key.java.abstraction.Field;
015: import de.uka.ilkd.key.java.abstraction.Type;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.logic.op.ProgramVariable;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: /* FieldSpecification
021: * taken from COMPOST and changed to achieve an immutable structure
022: */
023:
024: public class FieldSpecification extends VariableSpecification implements
025: Field {
026:
027: /**
028: * Field specification.
029: */
030:
031: public FieldSpecification() {
032: }
033:
034: public FieldSpecification(ProgramVariable var) {
035: this (var, var.getKeYJavaType());
036: }
037:
038: /**
039: * Field specification.
040: * @param var the ProgramVariable representing this concrete field
041: * @param type the Type of this field
042: */
043:
044: public FieldSpecification(ProgramVariable var, Type type) {
045: super (var, type);
046: }
047:
048: /**
049: * Field specification.
050: * @param var the ProgramVariable representing this concrete field
051: * @param init the Expression the field is initialised with.
052: * @param type the Type of this field
053: */
054:
055: public FieldSpecification(ProgramVariable var, Expression init,
056: Type type) {
057: super (var, init, type);
058: }
059:
060: /**
061: * Field specification.
062: * @param var the ProgramVariable representing this concrete field
063: * @param dimensions an int defining the dimension
064: * @param init the Expression the field is initialised with.
065: * @param type the Type of this field
066: */
067: public FieldSpecification(ProgramVariable var, int dimensions,
068: Expression init, Type type) {
069: super (var, dimensions, init, type, null);
070: }
071:
072: /**
073: * Field specification.
074: * @param children an ExtList with the children.
075: * May contain:
076: * an Expression (as initializer of the variable)
077: * a ProgramElementName (as name of the variable)
078: * a Comment
079: * @param var the ProgramVariable representing this concrete field
080: * @param dimensions an int defining the dimension
081: * @param type the Type of this field
082: */
083:
084: public FieldSpecification(ExtList children, ProgramVariable var,
085: int dimensions, Type type) {
086: super (children, var, dimensions, type);
087: }
088:
089: /**
090: * returns the name of the field as used in programs. In the logic
091: * each field has a unique name which is composed by the class name where
092: * it is declared and its source code name
093: *
094: * @return returns the name of the field as used in programs
095: */
096: public String getProgramName() {
097: return getProgramElementName().getProgramName();
098: }
099:
100: /**
101: * Test whether the declaration is static.
102: */
103: public boolean isStatic() {
104: return ((ProgramVariable) var).isStatic();
105: }
106:
107: /**
108: * Test whether the declaration is private.
109: */
110: public boolean isPrivate() {
111: return false;
112: }
113:
114: /**
115: * Test whether the declaration is protected.TO BE IMPLEMENTED
116: */
117:
118: public boolean isProtected() {
119: return false;
120: }
121:
122: /**
123: * Test whether the declaration is public.TO BE IMPLEMENTED
124: */
125:
126: public boolean isPublic() {
127: return false;
128: }
129:
130: /**
131: * Test whether the declaration is transient.TO BE IMPLEMENTED
132: */
133:
134: public boolean isTransient() {
135: return false;
136: }
137:
138: /**
139: * Test whether the declaration is volatile.TO BE IMPLEMENTED
140: */
141:
142: public boolean isVolatile() {
143: return false;
144: }
145:
146: /**
147: * Test whether the declaration is strictFp.TO BE IMPLEMENTED
148: */
149: public boolean isStrictFp() {
150: return false;
151: }
152:
153: /** calls the corresponding method of a visitor in order to
154: * perform some action/transformation on this element
155: * @param v the Visitor
156: */
157: public void visit(Visitor v) {
158: v.performActionOnFieldSpecification(this);
159: }
160:
161: }
|