2 User InterfaceTop1 Introduction

1 Introduction

This document describes the use of the RISC ProofNavigator, an interactive proving assistant for program and system reasoning developed at the Research Institute for Symbolic Computation (RISC).

Background

In the last two decades, a variety of interactive proving assistants and automatic theorem provers have emerged, e.g. PVS [12][14], Isabelle [11][9], Coq [3][7], or also the Theorema system developed at RISC [4][18]; see [19] for a comparative overview. Thus naturally the question arises what exactly the motivation is to develop yet another such tool. The overall context of the work presented in this document is the long-term objective to develop a program and system exploration environment that has a formal reasoning component at its core. Based on a number of use cases derived from the demands of such an environment (some of these cases are presented in this document), the author evaluated from 2004 to 2005 several prominent systems. The results were mixed.

While we achieved some quite good success (most notably with PVS), we also encountered various problems and nuisances, especially with the navigation within proofs, the presentation of proof states, the treatment of arithmetic, and the general interaction of the user with the systems; we frequently found that the elaboration of proofs was more difficult than we considered necessary. Without any doubt, some of these problems were caused by the author's inabilities and could be overcome by more training and experience with the corresponding systems (we only spent a couple of weeks on each) but such a demand already represents a considerable hurdle e.g. in educational scenarios. We felt that the learning curve for using a proving assistant should not be so steep.

From these experiments, we also draw a couple of important conclusions for the pragmatics of using a proving assistant:

Not all of the existing proving assistants meet these demands equally well; all in all, we were most satisfied with PVS (consequently various concepts in the RISC ProofNavigator were designed after the model of PVS, also its specification language is close to that of PVS). However, the PVS user interface has apparently come of age and the software is not open source which is especially a problem for its integration into a larger context.

The RISC ProofNavigator

Based on above investigations the author estimated that it would be fruitful to write from scratch a proof assistant according to his taste. Furthermore, this task should be possible with reasonable effort by making use of existing software that decides about the satisfiability of formulas over certain combinations of ground theories (and potentially performs related tasks such as formula simplification and counterexample generation); the really hard core logic and mathematics is in this software, not in the assistant itself. During the last couple of years, a couple of tools for solving this SMT (satisfiability modulo theories) problem have emerged, see the recently established SMT-LIB initiative and the associated SMT-COMP solver competition series [17]. After a (rather) short evaluation, we decided to use the Cooperating Validity Checker Lite (CVCL) Version 2.0 as a promising candidate [2][1]; it is open software, supports the most important theories needed for program verification, apparently shows good results, and its specification language is already close to that of PVS.

Thus we started in started in the fall of 2005 with the development of a new proving assistant. This document describes the result of our efforts called RISC ProofNavigator [15][16] that aims to meet the demands addressed above. The system is freely available under the GNU Public License at

http://www.risc.uni-linz.ac.at/research/formal/software/ProofNavigator

It has been reasonably well tested with (also large) verification examples but is certainly not free of bugs; error reports may be sent to the author at

Wolfgang.Schreiner@risc.uni-linz.ac.at

who commits himself to the maintenance of the software.

While most proving assistants are written in (semi-)declarative languages such as ML, Lisp, or Mathematica, the RISC ProofNavigator is implemented in Java, primarily for the following reasons: this language has free implementations with good performance on virtually every kind of machine, uses a runtime system with garbage collection (in the beginning of the 1990s still the exclusive domain of declarative languages and then a major reason to use these languages), has a rather clear semantics and supports modern programming language principles (a type system with interfaces and inheritance), is well supported by development frameworks, tools, and libraries, and has a large user community, in industry as well as in academia (many students nowadays learn programming in Java). These advantages are (for our purpose) more important than those of declarative languages, such as the simpler declarative semantics (ML) or the possibility to write programs in a rule-based style (Mathematica).

The graphical user interface of the RISC ProofNavigator is written with the help of the Eclipse Standard Widget Toolkit (SWT) which provides a Java wrapper for a native widget set of the underlying machine such that the user interface is responsive and good-looking; the SWT "browser" component is also the core of the system's presentation of proof states (which are rendered as documents containing a combination of XHTML and MathML [6]).

Document Structure

The remainder of the document is split in two parts:

Third Party Software

The RISC ProofNavigator uses the following third party software; detailed references can be found in the README file of the distribution:

Many thanks to the respective authors for their great work.


Wolfgang Schreiner

2 User InterfaceTop1 Introduction