Universität Bremen
FB3 AG BKB CXL

Literate Formal Software Development with Eclipse

Literate Formal Software Development with Eclipse is a project sponsered by IBM under the Eclipse Innovation Grant scheme. It aims at extending the Eclipse Platform to cover literate formal software development supported by a theorem prover. This will allow the development of formally verified, high-quality software inside a modern integrated development environment. The system is document-centred: specification and documentation are one document from which machine-checkable proof, documentation and program code are generated, and we treat this document as the central artefact constructed by the user ("literate specification").

This page gives an overview over our aims in this project. Over the course of the project, results will be published here too.

State of the art

The development of correct software is one of the core problems of computer science, and has a long history reaching back to its beginnings. Nevertheless, without some form of machine support to check the correctness of proofs and to deduct basic and trivial facts, completely formal development has in the past proved far too slow and cumbersome to be economically feasible.

However, the progress in theorem proving and automated deduction over the last fifteen years has made formal software development a viable proposition for systems where failure entails unacceptable risks. The foundations have been laid -- methodologies to support and guide the formal development such as development by transformation, theorem provers powerful enough to support formal development such as Isabelle, Coq or PVS, and specification languages encoded into these provers such as CASL.

One aspect still lacking is the user interface. Interfaces of modern provers are mostly command-line driven, rather basic and do not even come close to the comfort offered to todays' programmers with sophisticated IDEs such as the Eclipse platform.

Hence, it seems the next logical step to combine advances in user interface technology with advances in theorem proving and formal software development, and combine a modern IDE with a formal development tool. The generic nature, plug-in architecture and open-source status make the Eclipse platform an ideal choice for this.

Previous work

The project proposed here touches three rather diverse areas: formal program development, user interface technology for theorem provers, and document presentation. I feel that I am in a unique position to propose this project, as I can build on previous work in all these areas.

In detail, previous work includes the following projects:

  1. PGIP and PG/Kit.

    Together with David Aspinall and others, we have developed the PGIP protocol for interactive proof and the PG/Kit system implementing this protocol. This system can combine textual and graphical user interaction [2]. A PGIP connection for the Eclipse framework has already been implemented by David Aspinall and Daniel Winterstein in the 2004 Eclipse Innovation Grants "Eclipse Proof General", and we can build on this work.

    We have also organised the User Interfaces for Theorem Provers workshop UITP'03 in Rome (Sept. 2003), and are organising its 2005 incarnation as a satellite workshop the Joint European Conferences on Theory and Practice of Software, ETAPS'05.

  2. MMiSS

    The MMiSS project (Multi-Media Instructions for Safe Systems) developed a comprehensive Internet-based multimedia curriculum, covering the subject of safe systems. The curriculum is presented in a semantically structured document format developed for this purpose, together with a repository for fine-grained semantics-based version control and configuration management. From the MMiSS project, we can take the LaTeX-based document format, which in particular allows to embed texts such as source code or proof scripts into documents [1].

  3. TAS

    TAS [3] is a system for transformational program development based on the Isabelle theorem prover. Its main components are a generic implementation of window inferencing, a calculus for transformational proof, and a graphical user interface based on the principle of direct manipulation [4].

  4. AWE

    The AWE project investigates the systematic generalisation of given developments to more widely applicable transformation rules to aid reuse. We have implemented transformational development in Isabelle [6], and developed a methodology to generalise proofs in Isabelle [5]. The reuse aspect of this project has interesting links to the refactoring facilities as offered by Eclipse, and we plan to investigate these.

Proposed Project

The project proposed here will use the Eclipse platform to provide a tool for formal software development from specification down to executable programs. The central artefact is the specification, created by the user. The specification can be

We will support the formal program development in the transformational style, where transformations can be used to drive the development, based on our earlier work [5,6]. Transformations are pre-defined development steps which have been proven correct, and embody important design principles; they can be thought of as the formal equivalent of design patterns.

An important aspect of this is that we also support the informal aspects of specifications, that is specifications written in natural language or mathematical notation, and not read by a theorem prover. These informal aspects are particularly important in the first stages of the development process (such as requirements elicitation). Supporting them allows seamless support of the whole development process, starting with the first possibly even completely informal specification right down to executable code.

System Architecture

The architecture of the proposed system is not specific to any one prover, specification language or typesetting system. The first prototype will of course make specific choices here so we get something working soon. However, it is important to specify the interaction protocol of the different components very clearly so as to able to exchange them easily later. For these interaction protocols we can mostly use and build on our previous work.

Our system will implement Eclipse plug-ins to process literate specifications. The literate specification is the hub of the document flow. It is accessed by three modules, which in turn call external tools. Firstly, the PGIP plug-in extracts a proof script which it sends to an external theorem prover. Secondly, a document presentation plug-in typesets the document; in our first prototype, we will use LaTeX for this. And thirdly, we have a code extraction plug-in which generates executable code (if applicable) from the literate specification and runs it.

We will now describe the plug-ins in more detail.

  1. The PGIP plug-in allows interactive theorem provers to connect to Eclipse. The main function of the prover is to validate the script, but it will also send back messages about its current state which are essential while developing the proof script. The PGIP plug-in will communicate with the actual theorem provers. By using the generic PGIP protocol for interactive proof, we can reuse previous work from the 2004 Eclipse Innovation Grant "Eclipse Proof General" by David Aspinall and Daniel Winterstein for this purpose. Their PGIP plug-in will need to be extended to handle transformational development and visualise the development process. The actual formal development is modelled in the theorem prover; this guarantees the correctness of the development.

    In order to display the prover state, proof obligations and theorems we need a versatile user interface element (widget) that can interactively display mathematics in the same quality as produced for example by TeX. This will be implemented independent of the rest, and will be reusable for other Eclipse plug-ins as part of the SWT.

  2. A text formatting plug-in allows to display, edit and render structured text. The text will be semantically structured, such that designated parts can be read and processed by the theorem prover, but at the same time can be rendered in a typeset document. We plan to use the LaTeX format for this purpose in the first prototype, as it has an easily editable textual source format and an Eclipse plug-ins for it exists already (ecleTeX, LatEc) which can serve as the basis of this component. In a later stage of the project, we would like to use a WYSIWYG editor such as OpenOffice for this purpose, as LaTeX is a bit of a specialist language.

  3. The code extraction component allows to extract code from the literate specification. This is actually fairly trivial, because we just need to extract those sections marked as executable, but it could be expanded in future, for example to generate test sets generated from the specification along with the code.

References

 Web references: