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: * Created on 18.01.2005
11: */
12: package de.uka.ilkd.key.logic.op;
13:
14: import de.uka.ilkd.key.logic.Name;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
17: import de.uka.ilkd.key.logic.sort.Sort;
18:
19: /**
20: * Non-rigid function or predicate symbols are realised as instances
21: * of this class. Some particular non-rigid functions
22: * (namely attributes and arrays) are currently bypassing this class,
23: * but should be integrated into this framework in the mid-future (this
24: * was written 2005, may be you read this in the year 2035;-).
25: */
26: public class NonRigidFunction extends Function implements NonRigid {
27:
28: /**
29: * creates a non rigid function with given signature
30: * @param name the Name of the non-rigid function symbol
31: * @param sort the Sort of the symbol
32: * @param argSorts the array of Sort defining the argument sorts
33: */
34: public NonRigidFunction(Name name, Sort sort, Sort[] argSorts) {
35: super (name, sort, argSorts);
36: }
37:
38: /**
39: * creates a non rigid function with given signature
40: * @param name the Name of the non-rigid function symbol
41: * @param sort the Sort of the symbol
42: * @param argSorts the ArrayOfSort defining the argument sorts
43: */
44: public NonRigidFunction(Name name, Sort sort, ArrayOfSort argSorts) {
45: super (name, sort, argSorts);
46: }
47:
48: /**
49: * @return true if the value of "term" having this operator as
50: * top-level operator and may not be changed by modalities
51: */
52: public boolean isRigid(Term term) {
53: return false;
54: }
55:
56: public String proofToString() {
57: return "\\nonRigid " + super.proofToString();
58: }
59: }
|