INCREMENTAL SOFTWARE CONSTRUCTION WITH REFINEMENT DIAGRAMS

摘要

We propose here a mathematical framework for incremental software construc- tion and for 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 dkectly in terms of diagrams. A refinement diagram proof will be equivalent to a Hilbert like proof in lattice theory. We use refinement calculus as the logic for reasoning about software systems. The calculus models software parts as elements in a lattice of predicate transformers. In this way, we can use refinement diagrams to reason about the properties of software systems. We show here how to apply refinement diagrams and refinement calculus to the incremental construction of large software system. We concentrate on three topics: (ⅰ) modularization of software systems with component specifications and the role of information hiding in this approach, (ⅱ) layered extension of software by adding new features one-by-one and the role of inheritance and dynamic binding in this approach, and (ⅲ) evolution of software over time and the control of successive versions of software.