ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

escjava.prover
Class Harvey

java.lang.Object
  extended byescjava.prover.NewProver
      extended byescjava.prover.Harvey

public class Harvey
extends NewProver


Field Summary
(package private) static boolean debug
           
(package private)  SubProcess P
           
 
Fields inherited from class escjava.prover.NewProver
signature_defined, started
 
Constructor Summary
Harvey(boolean debug)
           
 
Method Summary
 ProverResponse declare_axiom(Formula formula)
          Declare a new axiom in the current theory.
 ProverResponse is_valid(Formula formula, java.util.Properties properties)
          Check the validity of the given formula given the current theory, its axioms, and the current set of assumptions.
static void main(java.lang.String[] argv)
           
 ProverResponse make_assumption(Formula formula)
          Make an assumption.
 ProverResponse retract_assumption(int count)
          Retract some assumptions.
 ProverResponse set_prover_resource_flags(java.util.Properties properties)
          Send arbitrary information to the prover.
 ProverResponse signature(Signature signature)
          Send the signature of a new theory to the prover.
 ProverResponse start_prover()
          Start up the prover.
 ProverResponse stop_prover()
          Stop the prover.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

P

SubProcess P

debug

static boolean debug
Constructor Detail

Harvey

public Harvey(boolean debug)
Method Detail

start_prover

public ProverResponse start_prover()
Description copied from class: NewProver
Start up the prover. After the prover is started correctly it should be ready to receive any of the commands embodied by all the other methods of this API.

Specified by:
start_prover in class NewProver
Returns:
a response code. A response code of ProverResponse.OK indicates that the prover started successfully and is ready to receive commands. A response code of ProverResponse.FAIL indicates that the prover did not start successfully and is not ready to receive commands. In the latter case, ProverResponse.FAIL.info can contain additional arbitrary information about the failure.

set_prover_resource_flags

public ProverResponse set_prover_resource_flags(java.util.Properties properties)
Description copied from class: NewProver
Send arbitrary information to the prover. Typically this information is not mandatory and is only suggestions or informative information from the front-end. This data is highly prover-dependent.

Specified by:
set_prover_resource_flags in class NewProver
Parameters:
properties - the set of property/value pairs to send to the prover.
Returns:
a response code.

signature

public ProverResponse signature(Signature signature)
Description copied from class: NewProver
Send the signature of a new theory to the prover. Note that an empty signature is denoted by an empty Signature object, not by a null value.

Specified by:
signature in class NewProver
Parameters:
signature - the signature of the new theory.
Returns:
a response code.

declare_axiom

public ProverResponse declare_axiom(Formula formula)
Description copied from class: NewProver
Declare a new axiom in the current theory.

Specified by:
declare_axiom in class NewProver
Parameters:
formula -
Returns:
a response code.

make_assumption

public ProverResponse make_assumption(Formula formula)
Description copied from class: NewProver
Make an assumption.

Specified by:
make_assumption in class NewProver
Parameters:
formula - the assumption to make.
Returns:
a response code.

retract_assumption

public ProverResponse retract_assumption(int count)
Description copied from class: NewProver
Retract some assumptions.

Specified by:
retract_assumption in class NewProver
Parameters:
count - the number of assumptions to retract.
Returns:
a response code.

is_valid

public ProverResponse is_valid(Formula formula,
                               java.util.Properties properties)
Description copied from class: NewProver
Check the validity of the given formula given the current theory, its axioms, and the current set of assumptions.

Specified by:
is_valid in class NewProver
Parameters:
formula - the formula to check.
properties - a set of hints, primarily resource bounds on this validity check.
Returns:
a response code.

stop_prover

public ProverResponse stop_prover()
Description copied from class: NewProver
Stop the prover.

Specified by:
stop_prover in class NewProver
Returns:
a response code.

main

public static void main(java.lang.String[] argv)

ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage