pat ::= T x
    | T(pat*) x
    | expr
    | expr.p(pat*)   <- predicate invocation
    | *		     <- "don't care"

form ::= expr == pat
     | T x = pat
     | form && form
     | form || form
     | forall ( form1 ) form2

predicate ::= predicate [T] x ( formals )
		directions { formula }
		...
		directions { stmt }


generalize command forms
 * guarded command
 - want implicit equality test, ability to write down patterns in a switch


take formula and get Java util iterator out of it
 - what happens if someone deletes from the iterator?
    - treat like an exception, write an exception handler in same
    class as predicate

???
syntax for throwing exception into formula solver
 - meaning of syntax given by predicate

**EXAMPLES**