    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    }