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.logic.Namespace;
22: import de.uka.ilkd.key.logic.TermBuilder;
23: import de.uka.ilkd.key.parser.jml.NotSupportedExpressionException;
24:
25: public abstract class JMLSpec extends TermBuilder {
26:
27: protected Namespace progVarNS = null;
28: protected Namespace funcNS = null;
29: protected NotSupportedExpressionException nsEx = null;
30:
31: public abstract LinkedHashMap getTerm2Old();
32:
33: public Namespace getProgramVariableNS() {
34: return progVarNS;
35: }
36:
37: public Namespace getFunctionNS() {
38: return funcNS;
39: }
40:
41: public void setInvalid(NotSupportedExpressionException nsEx) {
42: this .nsEx = nsEx;
43: }
44:
45: public boolean isValid() {
46: return nsEx == null;
47: }
48:
49: }
|