Appeared in: KORSO - Correct Software by Formal Methods, LNCS 1009
Abstract |
In this paper we present an approach towards a framework based on the type theory ECC (Extended Calculus of Constructions) in which specifications, programs and operators for modular development by stepwise refinement can be formally described and reasoned about. We demonstrate how generic software development steps can be expressed as higher-order functions and how proofs about their asserted effects can be carried out in the underlying logical calculus. For formalizing transformations that require syntactic manipulation of objects, we introduce a two-level system combining a meta-level and an object level and show how to express and reason about transformations that faithfully represent object-level operators.
Online Copy |
Available as Postscript (143 KB)
BibTeX Entry |
@incollection{vonHenke:95, author = "F.W. von Henke and A. Dold and H. Rue{\ss} and D. Schwier and M. Strecker", title = "Construction and Deduction Methods for the Formal Development of Software", booktitle = "{KORSO}, Correct Software by Formal Methods", editor = "M. Broy and S. J{\"a}hnichen", number = "1009", publisher = "Springer-Verlag, Lecture Notes in Computer Science", year = "1995" }
Last modified: Sat Nov 11 20:34:05 CET 2006 |