4 Future WorkTop2 User Interface3 Examples

3 Examples

In this chapter, we are going to illustrate the features of the RISC ProofNavigator by a series of small examples of specifications and proofs. The examples (that are included in the software distribution) are designed for consecutive study and introduce language and system features on demand, i.e., at those points where they are needed. A systematic presentation of these features is given in the appendix.


Wolfgang Schreiner

4 Future WorkTop2 User Interface3 Examples