D.  New RISC ProofNavigator

The RISC ProgramExplorer includes an updated version of the RISC ProofNavigator; as shown in Appendix E, the RISC ProgramExplorer may also be invoked in a mode that exposes only the RISC ProofNavigator interface and can be used very much like the original RISC ProofNavigator.

However, there are various differences between the new version of the RISC ProofNavigator and the original one:

Bug Fixes

The new version fixes various bugs of the original version; these fixes have not been propagated to the original version, i.e. the original version is not maintained any more. It is therefore strongly recommended to switch to the new version included in the RISC ProgramExplorer.

Interaction

On some occasions, the RISC ProofNavigator asks the user for input (e.g., whether the user really wants to quit). In the original version, the input was provided by text input from the command line. In the new version, a corresponding interaction window pops up.

Commands

The original RISC ProofNavigator supported the commands type, formula, value for printing the definition of a type, formula, or value; the command names could thus not be used as identifiers.

The new version calls these commands printt, printv, and printf.

Context Directories

The contents of the context directories have been stream-lined (see Appendix G).

Since these changes are only minor, we still refer to the original manual [5] for the documentation of the RISC ProofNavigator. However, in the future, the new version may further diverge from the original one.