|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
Extraction of structured programs from specification proofs
Crossley, John and Poernomo, Iman and Wirsing, Martin (2000) Extraction of structured programs from specification proofs. In: Recent Trends in Algebraic Development Techniques: 14th International Workshop, WADT ‘99, Chateau de Bonas, September 15-18, 1999 Selected Papers.
Official URL: http://www.springerlink.com/content/hu7wlq6gkkvu9jh0/
We present a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL. These programs are “correct” in the sense that they satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, is novel because it adds structural rules corresponding to the standard ways of modifying specifications: translating (renaming), taking unions, and hiding signatures. Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We use this to produce an executable refinement of a given specification and we then provide a method for producing a program module that maximally respects the original structure of the specification. Throughout the paper we demonstrate the technique with a simple example.
Repository Staff Only: item control page