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: package de.uka.ilkd.key.logic.op;
09:
10: import de.uka.ilkd.key.logic.Name;
11: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
12: import de.uka.ilkd.key.logic.sort.Sort;
13:
14: /**
15: * Instances of this classes represent non-rigid functions, which dependent only on the
16: * state of the heap and not of any local variables. This means their interpretation coincides
17: * on all states that describe the same heap.
18: *
19: * A famous representant of this kind of function is the <tt>inReachableState</tt> predicate.
20: */
21: public class NonRigidHeapDependentFunction extends NonRigidFunction {
22:
23: /**
24: * creates a non rigid function with given signature
25: * @param name the Name of the non-rigid function symbol
26: * @param sort the Sort of the symbol
27: * @param argSorts the array of Sort defining the argument sorts
28: */
29: public NonRigidHeapDependentFunction(Name name, Sort sort,
30: ArrayOfSort argSorts) {
31: super (name, sort, argSorts);
32: }
33:
34: /**
35: * creates a non rigid function with given signature
36: * @param name the Name of the non-rigid function symbol
37: * @param sort the Sort of the symbol
38: * @param argSorts the array of Sort defining the argument sorts
39: */
40: public NonRigidHeapDependentFunction(Name name, Sort sort,
41: Sort[] argSorts) {
42: super (name, sort, argSorts);
43: }
44:
45: public String proofToString() {
46: return "\\nonRigid[HeapDependent] "
47: + super .proofToString().substring(
48: "\\nonRigid ".length());
49: }
50: }
|