01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: //
17:
18: package de.uka.ilkd.key.speclang;
19:
20: import de.uka.ilkd.key.casetool.ModelMethod;
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
23: import de.uka.ilkd.key.logic.op.ListOfParsableVariable;
24: import de.uka.ilkd.key.logic.op.Modality;
25: import de.uka.ilkd.key.logic.op.ParsableVariable;
26: import de.uka.ilkd.key.logic.op.ProgramMethod;
27:
28: /**
29: * A contract about an operation, consisting of a precondition, a
30: * postcondition, a modifies clause, and a modality.
31: */
32: public interface OperationContract {
33: public ModelMethod getModelMethod();
34:
35: public ProgramMethod getProgramMethod(Services services);
36:
37: public Modality getModality();
38:
39: public FormulaWithAxioms getPre(ParsableVariable selfVar,
40: ListOfParsableVariable paramVars, Services services)
41: throws SLTranslationError;
42:
43: public FormulaWithAxioms getPost(ParsableVariable selfVar,
44: ListOfParsableVariable paramVars,
45: ParsableVariable resultVar, ParsableVariable excVar,
46: Services services) throws SLTranslationError;
47:
48: public SetOfLocationDescriptor getModifies(
49: ParsableVariable selfVar, ListOfParsableVariable paramVars,
50: Services services) throws SLTranslationError;
51: }
|