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: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016: //
017: package de.uka.ilkd.key.proof.init;
018:
019: import java.io.File;
020: import java.io.IOException;
021:
022: import de.uka.ilkd.key.logic.SetAsListOfChoice;
023: import de.uka.ilkd.key.logic.Term;
024: import de.uka.ilkd.key.logic.TermFactory;
025: import de.uka.ilkd.key.logic.op.Op;
026: import de.uka.ilkd.key.proof.ProblemLoader;
027: import de.uka.ilkd.key.proof.Proof;
028: import de.uka.ilkd.key.proof.ProofAggregate;
029: import de.uka.ilkd.key.proof.mgt.Contract;
030: import de.uka.ilkd.key.proof.mgt.Contractable;
031: import de.uka.ilkd.key.util.ProgressMonitor;
032:
033: /**
034: * This is the input type for JML enriched java source files or such
035: * source files in a directory tree structure
036: * @deprecated
037: */
038: public class JavaInput extends KeYUserProblemFile implements
039: ProofOblInput {
040:
041: File path = null;
042:
043: /**
044: * @param name
045: * @param path
046: * @param monitor
047: */
048: public JavaInput(String name, File path, ProgressMonitor monitor) {
049: super (name, path, monitor);
050: this .path = path;
051: }
052:
053: /* (non-Javadoc)
054: * @see de.uka.ilkd.key.proof.init.ProofOblInput#getPO()
055: */
056: public ProofAggregate getPO() {
057:
058: Term dummy = TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
059:
060: // create empty dummy proof to ensure the java model was loaded
061: return ProofAggregate.createProofAggregate(new Proof(
062: "dummy proof", dummy, "", getInitConfig()
063: .createTacletIndex(), getInitConfig()
064: .createBuiltInRuleIndex(), getInitConfig()
065: .getServices()), "dummy proof");
066: }
067:
068: /* (non-Javadoc)
069: * @see de.uka.ilkd.key.proof.init.EnvInput#getNumberOfChars()
070: */
071: public int getNumberOfChars() {
072: return 0;
073: }
074:
075: /** starts reading the input and modifies the InitConfig of this
076: * object with respect to the given modification strategy.
077: * @param mod the modification strategy to use
078: */
079: public void read(ModStrategy mod) throws ProofInputException {
080: return;
081: }
082:
083: /* (non-Javadoc)
084: * @see de.uka.ilkd.key.proof.init.KeYFile#readProblem(de.uka.ilkd.key.proof.init.ModStrategy)
085: */
086: public void readProblem(ModStrategy mod) throws ProofInputException {
087: return;
088: }
089:
090: /* (non-Javadoc)
091: * @see de.uka.ilkd.key.proof.init.ProofOblInput#askUserForEnvironment()
092: */
093: public boolean askUserForEnvironment() {
094: return false;
095: }
096:
097: /** returns the path to the Java model.
098: */
099: public String readJavaPath() throws ProofInputException {
100: String javaPath = null;
101: try {
102: javaPath = path.getCanonicalFile().getAbsolutePath();
103: } catch (IOException ioe) {
104: throw new ProofInputException(ioe);
105: }
106: return javaPath;
107: }
108:
109: /* (non-Javadoc)
110: * @see de.uka.ilkd.key.proof.init.KeYFile#readActivatedChoices()
111: */
112: public void readActivatedChoices() throws ProofInputException {
113: initConfig.setActivatedChoices(SetAsListOfChoice.EMPTY_SET);
114: }
115:
116: /* (non-Javadoc)
117: * @see de.uka.ilkd.key.proof.init.KeYFile#readIncludes()
118: */
119: public Includes readIncludes() throws ProofInputException {
120: return new Includes();
121: }
122:
123: /* (non-Javadoc)
124: * @see de.uka.ilkd.key.proof.init.KeYFile#getObjectOfContract()
125: */
126: public Contractable[] getObjectOfContract() {
127: return new Contractable[0];
128: }
129:
130: /* (non-Javadoc)
131: * @see de.uka.ilkd.key.proof.init.KeYFile#initContract(de.uka.ilkd.key.proof.mgt.Contract)
132: */
133: public boolean initContract(Contract ct) {
134: return false;
135: }
136:
137: /* (non-Javadoc)
138: * @see de.uka.ilkd.key.proof.init.KeYFile#readFuncAndPred(de.uka.ilkd.key.proof.init.ModStrategy)
139: */
140: public void readFuncAndPred(ModStrategy mod)
141: throws ProofInputException {
142: return;
143: }
144:
145: /* (non-Javadoc)
146: * @see de.uka.ilkd.key.proof.init.KeYFile#readSorts(de.uka.ilkd.key.proof.init.ModStrategy)
147: */
148: public void readSorts(ModStrategy mod) throws ProofInputException {
149: return;
150: }
151:
152: /* (non-Javadoc)
153: * @see de.uka.ilkd.key.proof.init.KeYFile#readRulesAndProblem(de.uka.ilkd.key.proof.init.ModStrategy)
154: */
155: public void readRulesAndProblem(ModStrategy mod)
156: throws ProofInputException {
157: return;
158: }
159:
160: /* (non-Javadoc)
161: * @see de.uka.ilkd.key.proof.init.KeYFile#readProof(de.uka.ilkd.key.proof.ProblemLoader)
162: */
163: public void readProof(ProblemLoader prl) throws ProofInputException {
164: return;
165: }
166: }
|