001 package escjava.prover;
002
003 import java.util.Properties;
004
005 public abstract class NewProver {
006
007 /*
008 * Variables indicating the state of the prover
009 */
010 public boolean started = false ;
011 public boolean signature_defined = false;
012
013 /**
014 * Start up the prover. After the prover is started correctly it
015 * should be ready to receive any of the commands embodied by all
016 * the other methods of this API.
017 *
018 * @return a response code. A response code of {@link
019 * ProverResponse#OK} indicates that the prover started successfully
020 * and is ready to receive commands. A response code of {@link
021 * ProverResponse#FAIL} indicates that the prover did not start
022 * successfully and is not ready to receive commands. In the latter
023 * case, {@link ProverResponse.FAIL.info} can contain additional
024 * arbitrary information about the failure.
025 */
026
027 /*@ public normal_behavior
028 @ assignable started;
029 @ ensures \result == ProverResponse.OK ||
030 @ \result == ProverResponse.FAIL;
031 @ ensures started;
032 @*/
033
034 public abstract /*@ non_null @*/ ProverResponse start_prover();
035
036 /**
037 * Send arbitrary information to the prover. Typically this
038 * information is not mandatory and is only suggestions or
039 * informative information from the front-end. This data is highly
040 * prover-dependent.
041 *
042 * @param properties the set of property/value pairs to send to the
043 * prover.
044 * @return a response code.
045 */
046 /*@ requires started;
047 @ ensures \result == ProverResponse.OK ||
048 @ \result == ProverResponse.FAIL ||
049 @ \result == ProverResponse.SYNTAX_ERROR ||
050 @ \result == ProverResponse.PROGRESS_INFORMATION;
051 @*/
052
053 public abstract /*@ non_null @*/ ProverResponse set_prover_resource_flags(/*@ non_null @*/ Properties properties);
054
055 /**
056 * Send the signature of a new theory to the prover.
057 *
058 * Note that an empty signature is denoted by an empty {@link
059 * Signature} object, <em>not</em> by a <code>null</code> value.
060 *
061 * @param signature the signature of the new theory.
062 * @return a response code.
063 */
064 /*@ requires started;
065 @ ensures \result == ProverResponse.OK ||
066 @ \result == ProverResponse.FAIL ||
067 @ \result == ProverResponse.SYNTAX_ERROR;
068 @*/
069
070 public abstract /*@ non_null @*/ ProverResponse signature(/*@ non_null @*/ Signature signature);
071
072 /**
073 * Declare a new axiom in the current theory.
074 *
075 * @param formula
076 * @return a response code.
077 */
078 /*@ requires started;
079 @ ensures \result == ProverResponse.OK ||
080 @ \result == ProverResponse.FAIL ||
081 @ \result == ProverResponse.SYNTAX_ERROR ||
082 @ \result == ProverResponse.INCONSISTENCY_WARNING;
083 @*/
084
085 public abstract /*@ non_null @*/ ProverResponse declare_axiom(/*@ non_null @*/ Formula formula);
086
087 /**
088 * Make an assumption.
089 *
090 * @param formula the assumption to make.
091 * @return a response code.
092 */
093 /*@ requires started;
094 @ ensures \result == ProverResponse.OK ||
095 @ \result == ProverResponse.FAIL ||
096 @ \result == ProverResponse.SYNTAX_ERROR ||
097 @ \result == ProverResponse.INCONSISTENCY_WARNING;
098 @*/
099
100 public abstract /*@ non_null @*/ ProverResponse make_assumption(/*@ non_null @*/ Formula formula);
101
102 /**
103 * Retract some assumptions.
104 *
105 * @param count the number of assumptions to retract.
106 * @return a response code.
107 */
108 /*@ requires started;
109 @ requires count >= 0 ;
110 @ ensures \result == ProverResponse.OK ||
111 @ \result == ProverResponse.FAIL;
112 @*/
113
114 public abstract /*@ non_null @*/ ProverResponse retract_assumption(int count);
115
116 /**
117 * Check the validity of the given formula given the current theory,
118 * its axioms, and the current set of assumptions.
119 *
120 * @param formula the formula to check.
121 * @param properties a set of hints, primarily resource bounds on
122 * this validity check.
123 * @return a response code.
124 *
125 * @design kiniry 30 June 2004 - Possible alternative names for this
126 * method include check(), is_entailed(), is_an_entailed_model_of().
127 * I prefer is_valid().
128 */
129 /*@ requires started;
130 @ ensures \result == ProverResponse.YES ||
131 @ \result == ProverResponse.NO ||
132 @ \result == ProverResponse.COUNTER_EXAMPLE ||
133 @ \result == ProverResponse.SYNTAX_ERROR ||
134 @ \result == ProverResponse.PROGRESS_INFORMATION ||
135 @ \result == ProverResponse.TIMEOUT ||
136 @ \result == ProverResponse.NO ||
137 @ \result == ProverResponse.FAIL;
138 @*/
139
140 public abstract /*@ non_null @*/ ProverResponse is_valid(/*@ non_null @*/ Formula formula,
141 Properties properties);
142
143 /**
144 * Stop the prover.
145 *
146 * @return a response code.
147 */
148 /*@ public normal_behavior
149 @ requires started;
150 @ assignable started;
151 @ ensures \result == ProverResponse.OK ||
152 @ \result == ProverResponse.FAIL;
153 @ ensures started == false;
154 @*/
155
156 public abstract /*@ non_null @*/ ProverResponse stop_prover();
157 }