Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
Screen decoration graphicsLogo

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.

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL:


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.

Item Type:Conference or Workshop Item (Paper)
ID Code:255
Deposited By:Dr Iman Poernomo
Deposited On:08 Nov 2007 17:15
Last Modified:06 Feb 2008 13:45

Repository Staff Only: item control page