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: package de.uka.ilkd.key.proof.init;
009:
010: import de.uka.ilkd.key.casetool.ModelMethod;
011: import de.uka.ilkd.key.cspec.ComputeSpecification;
012: import de.uka.ilkd.key.java.ArrayOfExpression;
013: import de.uka.ilkd.key.java.Statement;
014: import de.uka.ilkd.key.java.StatementBlock;
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.java.declaration.Modifier;
017: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
018: import de.uka.ilkd.key.java.declaration.VariableSpecification;
019: import de.uka.ilkd.key.java.expression.literal.NullLiteral;
020: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
021: import de.uka.ilkd.key.java.expression.operator.New;
022: import de.uka.ilkd.key.java.reference.TypeReference;
023: import de.uka.ilkd.key.java.statement.Branch;
024: import de.uka.ilkd.key.java.statement.Catch;
025: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
026: import de.uka.ilkd.key.java.statement.Try;
027: import de.uka.ilkd.key.logic.JavaBlock;
028: import de.uka.ilkd.key.logic.ProgramElementName;
029: import de.uka.ilkd.key.logic.Term;
030: import de.uka.ilkd.key.logic.TermBuilder;
031: import de.uka.ilkd.key.logic.op.*;
032: import de.uka.ilkd.key.proof.mgt.Contract;
033: import de.uka.ilkd.key.proof.mgt.Contractable;
034: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
035: import de.uka.ilkd.key.util.Debug;
036:
037: public class ComputeSpecificationPONew extends AbstractPO {
038:
039: private static final TermBuilder tb = TermBuilder.DF;
040:
041: private ModelMethod modelMethod;
042: private Modality modality;
043:
044: public ComputeSpecificationPONew(String name,
045: ModelMethod modelMethod) {
046: super (name, modelMethod.getContainingClass());
047:
048: this .modelMethod = modelMethod;
049: this .modality = Op.DIA;
050: }
051:
052: private JavaBlock buildJavaBlock(ProgramVariable[] formalParVars,
053: ProgramMethod programMethod, ProgramVariable selfVar,
054: ProgramVariable resultVar, ProgramVariable exceptionVar) {
055: //create method call
056: StatementBlock sb;
057: if (programMethod == null) {
058: //constructor
059: assert resultVar != null;
060: TypeReference typeRef = javaInfo
061: .createTypeReference(resultVar.getKeYJavaType());
062: New n = new New(formalParVars, typeRef, typeRef);
063: CopyAssignment copy = new CopyAssignment(resultVar, n);
064: sb = new StatementBlock(copy);
065: } else {
066: MethodBodyStatement call = new MethodBodyStatement(
067: programMethod, selfVar, resultVar,
068: new ArrayOfExpression(formalParVars));
069: sb = new StatementBlock(call);
070: }
071:
072: //create variables for try statement
073: KeYJavaType eType = javaInfo
074: .getTypeByClassName("java.lang.Throwable");
075: TypeReference excTypeRef = javaInfo.createTypeReference(eType);
076: ProgramElementName ePEN = new ProgramElementName("e");
077: ProgramVariable eVar = new LocationVariable(ePEN, eType);
078:
079: //create try statement
080: CopyAssignment nullStat = new CopyAssignment(exceptionVar,
081: NullLiteral.NULL);
082: VariableSpecification eSpec = new VariableSpecification(eVar);
083: ParameterDeclaration excDecl = new ParameterDeclaration(
084: new Modifier[0], excTypeRef, eSpec, false);
085: CopyAssignment assignStat = new CopyAssignment(exceptionVar,
086: eVar);
087: Catch catchStat = new Catch(excDecl, new StatementBlock(
088: assignStat));
089: Try tryStat = new Try(sb, new Branch[] { catchStat });
090: sb = new StatementBlock(new Statement[] { nullStat, tryStat });
091:
092: //create java block
093: JavaBlock result = JavaBlock.createJavaBlock(sb);
094:
095: return result;
096: }
097:
098: /**
099: * Returns the program method associated with this proof obligation.
100: */
101: private ProgramMethod getProgramMethod(
102: ListOfProgramVariable paramVars) {
103: //get class type
104: String className = modelClass.getFullClassName();
105: KeYJavaType classType = javaInfo.getTypeByClassName(className);
106: Debug.assertTrue(classType != null);
107:
108: //get program method
109: return javaInfo.getProgramMethod(classType, modelMethod
110: .getName(), paramVars.toArray(), classType);
111: }
112:
113: public void readProblem(ModStrategy mod) throws ProofInputException {
114: //make sure initConfig has been set
115: if (initConfig == null) {
116: throw new IllegalStateException("InitConfig not set.");
117: }
118:
119: //prepare variables, program method and container for @pre-functions
120: ListOfProgramVariable paramVars = buildParamVars(modelMethod);
121: ProgramMethod programMethod = getProgramMethod(paramVars);
122: ProgramVariable selfVar = null;
123: if (programMethod != null && !programMethod.isStatic()) {
124: selfVar = buildSelfVarAsProgVar();
125: }
126: ProgramVariable resultVar = buildResultVar(modelMethod);
127: ProgramVariable exceptionVar = buildExcVar();
128:
129: //create formal parameters
130: ProgramVariable[] parVars = paramVars.toArray();
131: ProgramVariable[] formalParVars = new ProgramVariable[parVars.length];
132: for (int i = 0; i < parVars.length; i++) {
133: ProgramElementName name = new ProgramElementName("_"
134: + parVars[i].name());
135: formalParVars[i] = new LocationVariable(name, parVars[i]
136: .getKeYJavaType());
137: registerInNamespaces(formalParVars[i]);
138: }
139:
140: final JavaBlock methodCallJavaBlock;
141: {
142: methodCallJavaBlock = buildJavaBlock(parVars,
143: programMethod, selfVar, resultVar, exceptionVar);
144: assert methodCallJavaBlock != null;
145: }
146:
147: // register created variables
148: registerInNamespaces(selfVar);
149: registerInNamespaces(paramVars);
150: registerInNamespaces(resultVar);
151: registerInNamespaces(exceptionVar);
152:
153: final Term resultTerm = ComputeSpecification
154: .createSpecificationComputationTerm(
155: methodCallJavaBlock, initConfig.progVarNS());
156:
157: //@todo resultTerm = precondition -> resultTerm (translating away OCL)
158: poTerms = new Term[1];
159: poTerms[0] = resultTerm;
160:
161: }
162:
163: public Contractable[] getObjectOfContract() {
164: return new Contractable[] { modelMethod };
165: }
166:
167: public boolean initContract(Contract ct) {
168: if (!(ct instanceof OldOperationContract)) {
169: return false;
170: }
171:
172: OldOperationContract mct = (OldOperationContract) ct;
173:
174: if (!(mct.getModelMethod().equals(modelMethod) && mct
175: .getModality().equals(modality))) {
176: return false;
177: }
178:
179: ct.addCompoundProof(getPO());
180: return true;
181: }
182:
183: }
|