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    }