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 }