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 SExp

    java.lang.Object
      escjava.prover.SExp

Direct Known Subclasses:
  Atom, SInt, SList

public abstract class SExp
extends java.lang.Object

S-Expression datatype for use in interfacing to the ESC Theorem prover, Simplify.

Considered as a language, the grammer of s-expressions is as follows:

       SExp ::= Atom | int | SList
       SList ::= ( SExp* )

That is, s-expressions consist of either an atom, an integer, or a possibly-empty list of s-expressions. `Atom`s are interned `String`s used to represent symbols.

Methods are available to test whether an `SExp` is an `Atom`, an integer, or a list. If the "type" of an `SExp` is known, it can be converted into what it represents. If an attempt is made to convert an `SExp` to an incorrect "type", the checked exception `SExpTypeError`will be thrown.``

`SExp`s can be printed onto a `PrintStream`.

See Also:
  `SExpTypeError`, `Atom`, `SList`

Constructor Summary
`(package private)` | `SExp()`

Method Summary
`static void` | `display(SExp x)` Display a `SExp` verbosely, using all its accessor methods.
`static SExp` | `fancyMake(java.lang.Object o)` Return an S-expression representing an integer (passed wrapped in an `Integer`), an atom (specified via a `String`), or an existing S-expression (this case leaves the argument unchanged).
`Atom` | `getAtom()` If we represent an atom, return it as an `Atom`; otherwise, throw `SExpTypeError`.
`int` | `getInteger()` If we represent an integer, return it as an `int`; otherwise, throw an `SExpTypeError`.
`SList` | `getList()` If we represent a list, return it as an `SList`; otherwise, throw `SExpTypeError`.
`boolean` | `isAtom()` Do we represent an atom?
`boolean` | `isInteger()`
`boolean` | `isList()` Do we represent a list?
`static void` | `main(java.lang.String[] args)` A simple test routine
`static SExp` | `make(int i)` Return an S-expression representing a given integer.
`abstract void` | `prettyPrint(java.io.PrintStream out)` Pretty-print a textual representation of us on a given `PrintStream`.
`void` | `print()` Print a textual representation of us on `System.out`.
`abstract void` | `print(java.io.PrintStream out)` Print a textual representation of us on a given `PrintStream`.
`java.lang.String` | `toString()`

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

Constructor Detail

### SExp

    SExp()

Method Detail

### make

    public static SExp make(int i)

  Return an S-expression representing a given integer.

  This is faster than using `fancyMake(new Integer(i))`.

### fancyMake

    public static SExp fancyMake(java.lang.Object o)

  Return an S-expression representing an integer (passed wrapped in an `Integer`), an atom (specified via a `String`), or an existing S-expression (this case leaves the argument unchanged).

### isAtom

    public boolean isAtom()

  Do we represent an atom?

### isInteger

    public boolean isInteger()

  Returns:
    a flag indicating if we represent an integer.

### isList

    public boolean isList()

  Do we represent a list?

### getAtom

    public Atom getAtom()
                 throws SExpTypeError

  If we represent an atom, return it as an `Atom`; otherwise, throw `SExpTypeError`.

  Throws:
    `SExpTypeError`

### getInteger

    public int getInteger()
                   throws SExpTypeError

  If we represent an integer, return it as an `int`; otherwise, throw an `SExpTypeError`.

  Throws:
    `SExpTypeError`

### getList

    public SList getList()
                  throws SExpTypeError

  If we represent a list, return it as an `SList`; otherwise, throw `SExpTypeError`.

  Throws:
    `SExpTypeError`

### print

    public abstract void print(java.io.PrintStream out)

  Print a textual representation of us on a given `PrintStream`.

  Note: This routine will take a `PrintWriter` instead when we switch to a more recent version of JDK.

### print

    public void print()

  Print a textual representation of us on `System.out`.

  (This is a convenience function.)

### prettyPrint

    public abstract void prettyPrint(java.io.PrintStream out)

  Pretty-print a textual representation of us on a given `PrintStream`.

  Note: This routine will take a `PrintWriter` instead when we switch to a more recent version of JDK.

### toString

    public java.lang.String toString()

  Returns:
    a textual representation of this s-expression.

### main

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

  A simple test routine

  Throws:
    `SExpTypeError`

### display

    public static void display(SExp x)
                        throws SExpTypeError

  Display a `SExp` verbosely, using all its accessor methods.

  This method is intended for test use.

  Throws:
    `SExpTypeError`

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