Construction and Deduction Methods
for the Formal Development of Software

F.W. von Henke, A. Dold , H. Rueß, D. Schwier, and M. Strecker

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