4 Future Work
The RISC ProofNavigator has shown its usefulness in several small and
not-so-small system verifications (some of which are contained in the software
distribution). However, there are several issues that require further work:
- Decision Procedures
- The system is currently bound to the
decision procedure CVCL Version 2.0 and does neither work with more
recent versions of CVCL nor with other decision procedures. This is not a
fundamental problem but a question of a mapping of the higher-order
specification language used by the RISC ProofNavigator to the first-order
languages supported by most provers and of corresponding software
interfaces. A diploma thesis has recently started corresponding
investigations.
- Specification Language
- The specification language of the system is very
simple and does not support various features than can be found in other
languages. For instance, it lacks the definition of recursive
algebraic datatypes with structural induction as a proof principle and also
a module system analogous to that of PVS. The introduction of corresponding
features will be triggered by the integration of the system into a larger
program reasoning framework.
- Rewriting Proofs
- The system is weak when it comes to proofs that
essentially depend on applying universally quantified equalities (or
equivalences or implications) as rewrite rules. For instance, the software
distribution contains an example specification arrays.pn with an
axiomatic characterization of arrays; based on this specification, the proof
of the extensionality principle corresponding to the one presented in
Section 3.2 becomes quite cumbersome. The
system should be extended to allow to mark formulas of a certain form as
"rewrite rules" that are automatically applied in proof state
simplifications (such features can be e.g. found in PVS and Isabelle).
- Proof Checking
- The system stores the individual commands invoked
in a proof for later replay; it does not generate proof objects
that describe the individual low-level reasoning steps performed by the
commands and that can be used for independent verification of a proof by an
external proof checker. Some decision procedures (e.g. CVCL) optionally
generate such objects as well as several interactive theorem provers (e.g.
CoQ or Isabelle). It would be worthwhile to investigate similar features for
the RISC ProofNavigator.
While some of above issues will be most probably tackled in the future, we
will mainly concentrate on the development of an program exploration
environment that integrates the RISC ProofNavigator as a reasoning
component. The demands of this environment will drive the further elaboration
of the software.
Wolfgang
Schreiner
