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 SExp

java.lang.Object
  extended byescjava.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. Atoms are interned Strings 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.

SExps 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

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