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.casetool.ModelClass;
013: import de.uka.ilkd.key.casetool.ModelManager;
014: import de.uka.ilkd.key.java.Recoder2KeY;
015: import de.uka.ilkd.key.logic.IteratorOfNamed;
016: import de.uka.ilkd.key.logic.op.Function;
017: import de.uka.ilkd.key.logic.op.ProgramVariable;
018: import de.uka.ilkd.key.proof.ProofAggregate;
019: import de.uka.ilkd.key.proof.RuleSource;
020:
021: /** Represents the proof obligation input for the prover as an OCL
022: * constraint in textual format.
023: * @deprecated Replaced by AbstractPO.
024: */
025: public abstract class OCLProofOblInput implements ProofOblInput {
026:
027: /** The initial configuration for a prover to use for reading and modify*/
028: protected InitConfig initConfig = null;
029: private String name;
030: private String proofHeader;
031:
032: private static ModelManager modelManager;
033:
034: public static void setModelManager(ModelManager modMan) {
035: if (modelManager == null) {
036: modelManager = modMan;
037: }
038: }
039:
040: public static ModelManager getModelManager() {
041: return modelManager;
042: }
043:
044: /** Creates a new representation of an OCL input with a name describing
045: * the kind of input.
046: */
047: public OCLProofOblInput(String name) {
048: this .name = name;
049: }
050:
051: /** returns the problems as generated by reading the OCL constraint
052: * and translating it to DL formulas.
053: */
054: public abstract ProofAggregate getPO();
055:
056: public void readActivatedChoices() throws ProofInputException {
057: //nothing to do
058: }
059:
060: public Includes readIncludes() throws ProofInputException {
061: RuleSource standard = RuleSource
062: .initRuleFile("standardRules.key");
063: Includes includes = new Includes();
064: includes.put("standardRules", standard);
065: return includes;
066: }
067:
068: String getProofHeader(String javaPath) {
069: if (proofHeader == null) {
070: proofHeader = createProofHeader(initConfig, javaPath);
071: }
072: return proofHeader;
073: }
074:
075: /** creates declarations necessary to save/load proof in textual form */
076: static String createProofHeader(InitConfig initConfig,
077: String javaPath) {
078: String s;
079: s = "\\javaSource \"" + javaPath + "\";\n\n";
080:
081: IteratorOfNamed it;
082:
083: /* program sorts need not be declared and
084: * there are no user-defined sorts with this kind of PO (yes?)
085: s += "sorts {\n"; // create declaration header for the proof
086: it = initConfig.sortNS().getProtocolled();
087: while (it.hasNext()) {
088: String n=it.next().toString();
089: int i;
090: if ((i=n.indexOf("."))<0 ||
091: initConfig.sortNS().lookup(new Name(n.substring(0,i)))==null) {
092: //the line above is for inner classes.
093: //KeY does not want to handle them anyway...
094: s = s+"object "+n+";\n";
095: }
096: }
097: s+="}
098: */
099: s += "\n\n\\programVariables {\n";
100: it = initConfig.progVarNS().getProtocolled();
101: while (it.hasNext())
102: s = s + ((ProgramVariable) (it.next())).proofToString();
103:
104: s += "}\n\n\\functions {\n";
105: it = initConfig.funcNS().getProtocolled();
106: while (it.hasNext()) {
107: Function f = (Function) it.next();
108: // only declare @pre-functions, others will be generated automat.
109: if (f.name().toString().indexOf("@pre") != -1) {
110: s += f.proofToString();
111: }
112: }
113:
114: s += "}\n\n";
115: return s;
116: }
117:
118: /** returns the initial configuration that is used to read the OCL
119: * input and that is used to be modified during reading.
120: */
121: public InitConfig getInitConfig() {
122: return initConfig;
123: }
124:
125: /** reads the OCL constraint and modifies the initial prover configuration
126: * according to the given modification strategy.
127: */
128: public abstract void readProblem(ModStrategy mod)
129: throws ProofInputException;
130:
131: /** returns false, that is the input never asks the user which
132: * environment he prefers
133: */
134: public boolean askUserForEnvironment() {
135: return false;
136: }
137:
138: /** sets the initial configuration that is used to read the OCL
139: * input and that is used to be modified during reading.
140: */
141: public void setInitConfig(InitConfig conf) {
142: this .initConfig = conf;
143: }
144:
145: public void startProtocol() {
146: initConfig.sortNS().startProtocol();
147: initConfig.funcNS().startProtocol();
148: initConfig.progVarNS().startProtocol();
149: }
150:
151: /** returns the name of the OCL proof obligation input.
152: */
153: public String name() {
154: return name;
155: }
156:
157: public abstract ModelClass getModelClass();
158:
159: /** computes the method specifications and stores the results in the
160: * SpecificationRepository which belongs to the ProofEnvironment of InitCfg
161: */
162: public void readSpecs() {
163: // do nothing, class obsolete
164: }
165:
166: protected Recoder2KeY getKeYJavaASTConverter() {
167: return new Recoder2KeY(initConfig.getServices(), initConfig
168: .namespaces());
169: }
170:
171: public String getJavaPath() {
172: return getModelClass().getRootDirectory();
173: }
174:
175: /**
176: * Converts an empty string to "true" and keeps it unchanged otherwise.
177: */
178: public static String normalizeConstraint(String aText) {
179: if (aText.equals("")) {
180: return "true";
181: } else {
182: return aText;
183: }
184: }
185:
186: }
|