Contents

• 1 Introduction
• 2 User Interface
• 3 Examples
• 3.1 An Induction Proof
• 3.2 A User-Defined Datatype
• 3.3 A Program Verification
• 3.4 Another Verification
• 4 Future Work
• References
• A Specification Language
• A.1 Types
• A.2 Values
• A.3 Declarations
• B System Commands
• B.1 Declaration Commands
• B.2 Control Commands
• B.3 Primary Commands
• B.4 Secondary Commands
• B.5 Basic Commands
• C System Installation
• C.1 README
• C.2 INSTALL
• D System Invocation
• E Context Directory
• F Grammar
• F.1 Lexical Grammar
• F.2 Syntactical Grammar
• Footnotes
• Contents