Construction and Deduction Methods for the Formal Development of Software

Book Chapter in "KORSO:Methods, Languages, and Tools for the Construction of Correct Software", LNCS 1009, © Springer-Verlag.

---

Authors

F.W. von Henke, Axel Dold, Harald Rueß, D. Schwier, M. Strecker

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.

gzipped postscript or postscript

BibTeX Entry

@InCollection{vHDRSS:KORSO95,
    author = "F.W. von Henke and Axel Dold and Harald Rue{\ss}} and Detlef Schwier and Martin Strecker",
    title = "Construction and deduction methods for the formal development of software",
    booktitle = "KORSO: Methods, Languages, and Tools for the Construction of Correct Software",
    editor = "Manfred Broy",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer-Verlag",
    number = "1009",
    year = 1995
}

---

Harald Ruess: ruess@csl.sri.com