Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.prover
Class Harvey

    java.lang.Object
      escjava.prover.NewProver
          escjava.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)

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage