Construction and Deduction Methods for the Formal Development of Software

. 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. 1 Introduction Modern software engineering regards software development as an evolutionary process [Wir95, BP81]. One view of this process is that, starting from abstract, high-level requirement specifications, a series of refinement or implementation steps is app..