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: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
11: // and Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16:
17: package de.uka.ilkd.key.jml;
18:
19: import java.util.LinkedHashMap;
20:
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.logic.Namespace;
23: import de.uka.ilkd.key.logic.NamespaceSet;
24: import de.uka.ilkd.key.logic.op.ProgramMethod;
25:
26: /**
27: * A generic method spec used to desugar the pure modifier:
28: *
29: * behavior
30: * assignable \nothing;
31: */
32: public class JMLPuritySpec extends JMLMethodSpec {
33:
34: public JMLPuritySpec(ProgramMethod md, Services services,
35: Namespace params, LinkedHashMap term2old,
36: JMLClassSpec cSpec, NamespaceSet nss, String javaPath) {
37: super (md, services, params, term2old, cSpec, nss, javaPath);
38: this .setAssignableMode("nothing");
39: }
40:
41: public String toString() {
42: return "Purity specification for method " + pm.getName()
43: + " \nin context " + cd.getName();
44: }
45: }
|