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 Simplify

    java.lang.Object
      escjava.prover.Simplify

public class Simplify
extends java.lang.Object

The interface to the Simplify theorem prover program using Strings to send and S-expressions to receive.

Note that a Java application will not exit normally (i.e., when its `main()` method returns) until all subprocesses have finished. In particular, this implies that all `Simplify` instances must be closed before this can occur. Alternatively, a Java application can just call `java.lang.System.exit` to force an exit to occur without waiting for subprocesses.

Warning: This class uses `SubProcess.readSExp()`, which does not implement the full grammer for SExps. See that routine for the exact limitations.

See Also:
  `SExp`, `SubProcess`, `CECEnum`

Field Summary
`private SubProcess` | `P` Our Simplify subprocess; no actions should be taken on this subprocess unless `readySubProcess()` is called first.
`private CECEnum` | `subProcessUser` This variable holds the `CECEnum` that is currently using Simplify (there can be at most 1 such CECEnum), or `null` if there is no such CECEnum.

Constructor Summary
`Simplify()` Create a new invocation of Simplify as a sub-process.

Method Summary
`void` | `close()` Close us.
`private void` | `eatPrompt()` Consume the prompt from our Simplify subprocess.
`(package private) static void` | `exhaust(java.util.Enumeration n)` Force an `Enumeration` to compute all of its elements
`static void` | `main(java.lang.String[] args)` A simple test routine
`java.util.Enumeration` | `prove(java.lang.String exp)` Attempt to verify expression `exp`.
`private void` | `readySubProcess()` Prepare Simplify for use.
`void` | `sendCommand(java.lang.String s)` Send a single `String` command to Simplify.
`void` | `sendCommands(java.lang.String s)` Send a `String` containing zero-or-more commands to our Simplify subprocess.
`void` | `startProve()` Readies the simplify subprocess and sets its user to this, but send no commands.
`java.util.Enumeration` | `streamProve()`
`java.io.PrintStream` | `subProcessToStream()`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### P

    private final SubProcess P

  Our Simplify subprocess; no actions should be taken on this subprocess unless `readySubProcess()` is called first.

### subProcessUser

    private CECEnum subProcessUser

  This variable holds the `CECEnum` that is currently using Simplify (there can be at most 1 such CECEnum), or `null` if there is no such CECEnum.

  Simplify is available for use iff this is `null`. Use `readySubProcess()` to make Simplify available.

Constructor Detail

### Simplify

    public Simplify()

  Create a new invocation of Simplify as a sub-process.

  The resulting invocation is initially open, but may be closed permanently with the `close()` method.

  This constructor may result in a fatal error if any problems occur.

Method Detail

### readySubProcess

    private void readySubProcess()

  Prepare Simplify for use.

  Precondition: we are not closed.

  Ensures any `CECEnum` currently using Simplify finishes.

### close

    public void close()

  Close us.

  This destroys the associated subprocess. Afterwards, none of our methods should ever be called again. Likewise, no methods of any `Enumeration` we've returned should ever be called again.

  This method may result in a fatal error if any problems occur. Our subprocess is guaranteed to be destroyed afterwards, regardless of which exit is taken.

### sendCommand

    public void sendCommand(java.lang.String s)

  Send a single `String` command to Simplify.

  A command is something that produces no output other than whitespace and a prompt. If any other output is produced, a fatal error will result.

  Precondition: we are not closed.

  Parameters:
    `s` - the string containing the command to be sent to simplify.

### sendCommands

    public void sendCommands(java.lang.String s)

  Send a `String` containing zero-or-more commands to our Simplify subprocess.

  A command is something that produces no output other than whitespace and a prompt. If any other output is produced, a fatal error will result.

  Precondition: we are not closed.

  Parameters:
    `s` - the string containing the commands to be sent to simplify.

### prove

    public java.util.Enumeration prove(java.lang.String exp)

  Attempt to verify expression `exp`.

  We always return an `Enumeration` of non-`null` `SimplifyOutput`s. If verifying `exp` succeeds, the resulting `Enumeration` will end with a `SimplifyOutput` of kind `SimplifyOutput.VALID`.

  Precondition: we are not closed, and `exp` is properly formed according to Simplify's rules.

### startProve

    public void startProve()

  Readies the simplify subprocess and sets its user to this, but send no commands.

### streamProve

    public java.util.Enumeration streamProve()

### subProcessToStream

    public java.io.PrintStream subProcessToStream()

### eatPrompt

    private void eatPrompt()

  Consume the prompt from our Simplify subprocess. If the next output characters are not exactly the prompt (possibly preceeded by some whitespace), a fatal error is reported.

  Precondition: we are not closed.

### main

    public static void main(java.lang.String[] args)
                     throws java.io.IOException

  A simple test routine

  Throws:
    `java.io.IOException`

### exhaust

    static void exhaust(java.util.Enumeration n)

  Force an `Enumeration` to compute all of its elements

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