ProverEditorExplanation

WikiInclude(ProverEditorDescription)

Originally developed for JACK, it has now been integrated in the MOBIUS environment. See (BBC+06) for more information.

The basic idea behind the design of the MOBIUS Prover Editor is that reading and writing large-scale formal specifications is much the same as reading and writing large-scale program source (Kin04). Common programming interface idioms like outline views, syntax highlighting, (possibly type-aware) identifier completion, file and construct templates, etc. are naturally adopted and adapted to support development of, and reasoning about, formal models expressed in higher-order provers.

Additionally, the human-computer interface between the user and the prover via the Mobius PVE must not only be simple, but most importantly, familiar to traditional interactive prover users. Thus, most standard key bindings for the Emacs-based front-end are available from within the MOBIUS Prover Editor.

While the MOBIUS Prover Editor primarily supports Coq, development is underway to also support the PVS theorem prover, porting the improvements previously identified by (KO03), and reemphasizing the Prover Editor's prover-generic nature.

Version: 1 Time: Fri Mar 28 17:56:18 2008 Author: dcochran (dcochran) IP: 193.1.132.32