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: //
09: //
10: package de.uka.ilkd.key.proof.init;
11:
12: import de.uka.ilkd.key.proof.ProofAggregate;
13: import de.uka.ilkd.key.proof.mgt.Contract;
14: import de.uka.ilkd.key.proof.mgt.Contractable;
15:
16: /**
17: * Represents something that produces an input proof obligation for the
18: * prover. A .key file or a proof obligation generated from a CASE tool may
19: * be instances. An instance can be called to set an initial configuration,
20: * that is modified during reading the input (using <code>setInitConfig</code>),
21: * to get the read proof
22: * obligation (using <code>getProblemTerm</code>). During reading the input
23: * given initial configuration may become modified. The modification
24: * can be controlled by a modification strategy.
25: */
26: public interface ProofOblInput {
27:
28: /** returns the name of the proof obligation input.
29: */
30: String name();
31:
32: boolean askUserForEnvironment();
33:
34: /** Set the initial configuration used to read the input. It may become
35: * modified during reading depending on the modification strategy used
36: * for reading. Must be called before calling any of the read* methods.
37: */
38: void setInitConfig(InitConfig i);
39:
40: void readActivatedChoices() throws ProofInputException;
41:
42: void readSpecs();
43:
44: void readProblem(ModStrategy mod) throws ProofInputException;
45:
46: /** returns the proof obligation term as result of the proof obligation
47: * input. If there is still no input available because nothing has
48: * been read yet null is returned.
49: */
50: ProofAggregate getPO();
51:
52: Contractable[] getObjectOfContract();
53:
54: boolean initContract(Contract ct);
55: }
|