Contents
1  Introduction
2  User Interface
3  Programs, Theories, and Specifications
 3.1  Computing Factorial Numbers
 3.2  Searching for Records
 3.3  Failed Tasks and Interactive Proofs
4  Semantics and Verification
 4.1  Computing Factorial Numbers
 4.2  Recursive Computation of Factorials
 4.3  Searching in Arrays
 4.4  Program States and Control Flow Interruptions
 4.5  Objects and Method Side Effects
References
A  Programs as State Relations
B  Programming Language
C  Specification Language
 C.1  Logic Language
 C.2  Theory Definitions
 C.3  Class Specifications
 C.4  Class Invariants
 C.5  Method Specifications
 C.6  Loop Specifications
 C.7  Statement Specifications
D  New RISC ProofNavigator
E  Software Invocation
F  Software Installation
 F.1  README
 F.2  INSTALL
G  Task Directories
H  Grammars
 H.1  Programming Language
 H.2  Specification Language