|
Class Summary |
| CmdAssume |
An Assume command pushes some proposition onto the assumption stack
of the session. |
| CmdCheck |
A Check command takes a given proposition and asks the Session to
prove it. |
| CmdRaw |
A Raw command provides no additional structure, allowing arbitrary
commands (as long as they have no ouput) to be sent to the
prover. |
| CmdUndoAssume |
An UndoAssume command removes an assumption from the assumption
stack of the given session. |
| InvariantLemma |
InvariantLemmas are Lemmas created by printing a Daikon invariant
in Simplify format, sometimes with some hacks. |
| Lemma |
A lemma is an object that wraps a Simplify formula representing
some logical statement. |
| LemmaStack |
A stack of Lemmas that shadows the stack of assumptions that
Simplify keeps. |
| Session |
A session is a channel to the Simplify theorem-proving tool. |
| SessionManager |
A SessionManager is a component which handles the threading
interaction with the Session. |
| SimpUtil |
Utility functions for the simplify package. |