Incremental Software Construction with Refinement Diagrams

We propose here a mathematical framework for

incremental software construction

and

controlled software evolution

. The framework allows incremental changes of a software system to be described on a high architecture level, but still with mathematical precision so that we can reason about the correctness of the changes. The framework introduces

refinement diagrams

as a visual way of presenting the architecture of large software systems. Refinement diagrams are based on lattice theory and allow reasoning about lattice elements to be carried out directly in terms of diagrams. A refinement diagram proof will be equivalent to a Hilbert like proof in lattice theory. We show how to apply refinement diagrams and refinement calculus to the incremental construction of large software system. We concentrate on three topics: (i)

modularization

of software systems with component specifications and the role of information hiding in this approach, (ii)

layered extension

of software by adding new features one-by-one and the role of inheritance and dynamic binding in this approach, and (iii)

evolution of software

over time and the control of successive versions of software.