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.abstraction;
12:
13: import de.uka.ilkd.key.logic.op.IProgramVariable;
14:
15: /**
16: A program model element representing fields.
17: @author AL
18: @author RN
19: The file has been modified by the KeY team.
20: */
21: public interface Field extends Variable, Member {
22:
23: /**
24: * returns the program variable associated with this field
25: * @return the program variable associated with this field
26: */
27: IProgramVariable getProgramVariable();
28:
29: /**
30: * returns the name of the field as used in programs. In the logic
31: * each field has a unique name which is composed by the class name where
32: * it is declared and its source code name
33: *
34: * @return returns the name of the field as used in programs
35: */
36: String getProgramName();
37:
38: }
|