A formalisation of design structures

The authors present the formalization of methodological principles for developing large and complex software systems. They address the issues of information hiding that arise in hierarchical structured and componentwise-specified software systems using a binary implementation relation. They introduce a formally defined notion of design as a concept leading to definitions of black-box correctness (based on the exclusive use of specifications) and glass-box correctness (using implementation knowledge). The authors show the methodological soundness of black-box correctness and give an example demonstrating the pitfalls that can result from glass-box correctness. This is done in the framework of an algebraic approach to module composition using a version of lambda calculus for parameterization. The concepts are illustrated by small examples written in COLD