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:
018: package de.uka.ilkd.key.speclang.jml;
019:
020: import java.util.Map;
021:
022: import de.uka.ilkd.key.casetool.ModelMethod;
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
025: import de.uka.ilkd.key.logic.Term;
026: import de.uka.ilkd.key.logic.op.ListOfParsableVariable;
027: import de.uka.ilkd.key.logic.op.LogicVariable;
028: import de.uka.ilkd.key.logic.op.Modality;
029: import de.uka.ilkd.key.logic.op.ParsableVariable;
030: import de.uka.ilkd.key.logic.op.ProgramVariable;
031: import de.uka.ilkd.key.speclang.AbstractOperationContract;
032: import de.uka.ilkd.key.speclang.FormulaWithAxioms;
033:
034: public class JMLOperationContract extends AbstractOperationContract {
035: private final String originalDiverges;
036: private final boolean terminationCase;
037: private final String originalRequires;
038: private final String originalEnsures;
039: private final String originalSignals;
040: private final String originalAssignable;
041:
042: public JMLOperationContract(ModelMethod modelMethod,
043: String originalDiverges, boolean terminationCase,
044: String originalRequires, String originalEnsures,
045: String originalSignals, String originalAssignable) {
046: super (modelMethod, terminationCase ? Modality.DIA
047: : Modality.BOX);
048: this .originalDiverges = originalDiverges;
049: this .terminationCase = terminationCase;
050: this .originalRequires = originalRequires;
051: this .originalEnsures = originalEnsures;
052: this .originalSignals = originalSignals;
053: this .originalAssignable = originalAssignable;
054: }
055:
056: public FormulaWithAxioms getPre(ParsableVariable selfVar,
057: ListOfParsableVariable paramVars, Services services) {
058: JMLTranslator translator = services.getJMLTranslator();
059:
060: FormulaWithAxioms required = translator.translateRequires(
061: originalRequires, selfVar, paramVars);
062: Term resultFormula = required.getFormula();
063: Map resultAxioms = required.getAxioms();
064: resultAxioms.putAll(required.getAxioms());
065:
066: if (terminationCase) {
067: FormulaWithAxioms diverges = translator.translateDiverges(
068: originalDiverges, selfVar, paramVars);
069: resultFormula = tb.and(resultFormula, tb.not(diverges
070: .getFormula()));
071: resultAxioms.putAll(diverges.getAxioms());
072: }
073:
074: return new FormulaWithAxioms(resultFormula, resultAxioms);
075: }
076:
077: public FormulaWithAxioms getPost(ParsableVariable selfVar,
078: ListOfParsableVariable paramVars,
079: ParsableVariable resultVar, ParsableVariable excVar,
080: Services services) {
081: JMLTranslator translator = services.getJMLTranslator();
082:
083: FormulaWithAxioms ensures = translator.translateEnsures(
084: originalEnsures, selfVar, paramVars, resultVar, excVar);
085: FormulaWithAxioms signals = translator.translateSignals(
086: originalSignals, selfVar, paramVars, resultVar, excVar);
087:
088: Term excVarTerm;
089: if (excVar instanceof ProgramVariable) {
090: excVarTerm = tb.var((ProgramVariable) excVar);
091: } else {
092: excVarTerm = tb.var((LogicVariable) excVar);
093: }
094: Term excNullTerm = tb.equals(excVarTerm, tb.NULL(services));
095:
096: Term resultFormula = tb.ife(excNullTerm, ensures.getFormula(),
097: signals.getFormula());
098: Map resultAxioms = ensures.getAxioms();
099: resultAxioms.putAll(signals.getAxioms());
100:
101: return new FormulaWithAxioms(resultFormula, resultAxioms);
102: }
103:
104: public SetOfLocationDescriptor getModifies(
105: ParsableVariable selfVar, ListOfParsableVariable paramVars,
106: Services services) {
107: return services.getJMLTranslator().translateAssignable(
108: originalAssignable, selfVar, paramVars);
109: }
110: }
|