001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: package de.uka.ilkd.key.proof.init;
011:
012: import de.uka.ilkd.key.java.abstraction.ArrayType;
013: import de.uka.ilkd.key.java.abstraction.Type;
014: import de.uka.ilkd.key.jml.JMLSpec;
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.logic.op.Function;
017: import de.uka.ilkd.key.logic.op.ProgramMethod;
018: import de.uka.ilkd.key.logic.op.ProgramVariable;
019: import de.uka.ilkd.key.proof.mgt.Contract;
020: import de.uka.ilkd.key.proof.mgt.Contractable;
021: import de.uka.ilkd.key.proof.mgt.JavaModelMethod;
022: import de.uka.ilkd.key.util.KeYExceptionHandler;
023:
024: public abstract class JMLProofOblInputImpl implements JMLProofOblInput {
025:
026: protected JMLSpec spec = null;
027: protected ProgramMethod pm = null;
028: protected InitConfig initConfig = null;
029: protected String javaPath = null;
030: protected KeYExceptionHandler exceptionHandler = null;
031: protected boolean allInv = false;
032:
033: protected JMLProofOblInputImpl(JMLSpec spec, String javaPath,
034: boolean allInv) {
035: this .spec = spec;
036: this .javaPath = javaPath;
037: this .allInv = allInv;
038: }
039:
040: /**
041: * sets the exception handler used to collect occured errors
042: */
043: public void setExceptionHandler(KeYExceptionHandler keh) {
044: exceptionHandler = keh;
045: }
046:
047: public boolean initContract(Contract ct) {
048: return false;
049: }
050:
051: public boolean askUserForEnvironment() {
052: return false;
053: }
054:
055: /**
056: * Checks if the methods used in the specification that underlies this
057: * JMLProofOblInput are declared with the modifier pure.
058: */
059: public abstract boolean checkPurity();
060:
061: public void read(ModStrategy mod) throws ProofInputException {
062: }
063:
064: /**
065: * The Java Model is already initialized;
066: */
067: public String readModel() throws ProofInputException {
068: return null;
069: }
070:
071: public void initJavaModelSettings(String path) {
072: }
073:
074: /** returns the path to the Java model.
075: */
076: public String getJavaPath() {
077: return javaPath;
078: }
079:
080: /** set the initial configuration used to read an input. It may become
081: * modified during reading depending on the modification strategy used
082: * for reading.
083: */
084: public void setInitConfig(InitConfig i) {
085: initConfig = i;
086: }
087:
088: /** Specs have already been read.
089: */
090: public void readSpecs() {
091: }
092:
093: public void readActivatedChoices() throws ProofInputException {
094: //nothing to do
095: }
096:
097: /** reads the include section and returns an Includes object.
098: */
099: public Includes readIncludes() throws ProofInputException {
100: return new Includes();
101: }
102:
103: /** returns the name of the proof obligation input.
104: */
105: public String name() {
106: return spec.toString();
107: }
108:
109: public Contractable[] getObjectOfContract() {
110: return new Contractable[] { new JavaModelMethod(pm, javaPath,
111: initConfig.getServices()) };
112: }
113:
114: public void startProtocol() {
115: // do nothing
116: }
117:
118: public String createProgramVarsSection() {
119: IteratorOfNamed it = initConfig.progVarNS().allElements()
120: .iterator();
121: String result = "\\programVariables {\n";
122: while (it.hasNext()) {
123: final ProgramVariable pv = (ProgramVariable) it.next();
124: final Type javaType = pv.getKeYJavaType().getJavaType();
125: if (javaType instanceof ArrayType) {
126: result += ((ArrayType) javaType)
127: .getAlternativeNameRepresentation()
128: + " " + pv.name() + ";\n";
129: } else {
130: result += javaType.getFullName() + " " + pv.name()
131: + ";\n";
132: }
133: }
134: result += "}\n";
135: return result;
136: }
137:
138: public String createFunctionSection() {
139: IteratorOfNamed it = spec.getFunctionNS().allElements()
140: .iterator();
141: String result = "\\functions {\n";
142: while (it.hasNext()) {
143: Function f = (Function) it.next();
144: result += f.proofToString();
145: }
146: result += "}\n";
147: return result;
148: }
149:
150: public String createJavaSection() {
151: return "\\javaSource \"" + getJavaPath() + "\";\n";
152: }
153:
154: public String createProblemHeader() {
155: return createJavaSection() + "\n" + createProgramVarsSection()
156: + "\n" + createFunctionSection() + "\n";
157: }
158: }
|