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:
011: package de.uka.ilkd.key.gui;
012:
013: import java.util.Vector;
014:
015: import de.uka.ilkd.key.collection.ListOfString;
016: import de.uka.ilkd.key.java.JavaInfo;
017: import de.uka.ilkd.key.java.Services;
018: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
019: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
020: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
021: import de.uka.ilkd.key.jml.*;
022: import de.uka.ilkd.key.logic.op.ProgramMethod;
023: import de.uka.ilkd.key.proof.init.*;
024:
025: public class JMLEclipseAdapter implements JMLPOAndSpecProvider {
026:
027: KeYMediator mediator;
028: Services services;
029: String javaPath;
030: ProgramMethod m = null;
031: Implementation2SpecMap ism = null;
032: JavaInfo ji;
033: private boolean mainVisible = true;
034:
035: public JMLEclipseAdapter(KeYMediator mediator) {
036: services = mediator.getServices();
037: ji = services.getJavaInfo();
038: ism = services.getImplementation2SpecMap();
039: this .mediator = mediator;
040: javaPath = mediator.getProof().env().getJavaModel()
041: .getModelDir();
042: }
043:
044: public Vector getMethodSpecs(String className, String methodName,
045: ListOfString sigStrings) {
046: ListOfKeYJavaType signature = getSignature(sigStrings);
047: KeYJavaType classType = ji.getKeYJavaTypeByClassName(className);
048: m = ji.getProgramMethod(classType, methodName, signature,
049: classType);
050: if (!m.getMethodDeclaration().isAbstract()) {
051: SetOfJMLMethodSpec specs = ism.getSpecsForMethod(m);
052: JMLClassSpec cSpec = ism.getSpecForClass(classType);
053: if (specs != null) {
054: specs = specs.union(services
055: .getImplementation2SpecMap()
056: .getInheritedMethodSpecs(m, classType));
057: } else {
058: specs = ism.getInheritedMethodSpecs(m, classType);
059: }
060: if (specs != SetAsListOfJMLMethodSpec.EMPTY_SET
061: || cSpec != null) {
062: Vector specVector = new Vector();
063: if (specs != null) {
064: IteratorOfJMLMethodSpec it = specs.iterator();
065: while (it.hasNext()) {
066: JMLMethodSpec mSpec = it.next();
067: specVector.add(mSpec);
068: if (mSpec.replaceModelFieldsInAssignable() != null) {
069: specVector
070: .add(new AssignableCheckProofOblInput(
071: mSpec, javaPath));
072: }
073: }
074: }
075: if (cSpec != null && (cSpec.containsInvOrConst())) {
076: specVector.add(cSpec);
077: }
078: return specVector;
079: }
080: }
081: return null;
082: }
083:
084: public void createPOandStartProver(JMLSpec spec, boolean allInv,
085: boolean invPost, boolean assignable) {
086: ProofOblInput poi = null;
087: if (spec instanceof JMLMethodSpec) {
088: if (assignable) {
089: poi = new AssignableCheckProofOblInput(
090: (JMLMethodSpec) spec, javaPath);
091: ((AssignableCheckProofOblInput) poi)
092: .setAllInvariants(allInv);
093: } else if (invPost) {
094: poi = new JMLPostAndInvPO((JMLMethodSpec) spec,
095: javaPath, allInv);
096: } else {
097: poi = new JMLPostPO((JMLMethodSpec) spec, javaPath,
098: allInv);
099: }
100: } else if (spec instanceof JMLClassSpec) {
101: poi = new JMLInvPO((JMLClassSpec) spec, m, javaPath, allInv);
102: }
103: ProblemInitializer pi = new ProblemInitializer(Main
104: .getInstance(mainVisible));
105: try {
106: pi.startProver(mediator.getProof().env(), poi);
107: } catch (ProofInputException e) {
108: //too bad
109: }
110: }
111:
112: private ListOfKeYJavaType getSignature(ListOfString l) {
113: de.uka.ilkd.key.collection.IteratorOfString it = l.iterator();
114: ListOfKeYJavaType result = SLListOfKeYJavaType.EMPTY_LIST;
115: while (it.hasNext()) {
116: result = result.append(ji.getKeYJavaType(it.next()));
117: }
118: return result;
119: }
120:
121: public void setMainVisible(boolean mainVisible) {
122: this.mainVisible = mainVisible;
123: }
124:
125: }
|