DESIGNS AS FORMAL ENTITIES

A formal system consists of a set of axioms – that is, formulas or assertions that are assumed or known to be true – and a set of inference or proof rules that allows one to make deductions. Given a formal system a formal proof of an assertion or formula F consists of a finite sequence of formulas

F1, F2, …, Fn = F

such that each Fi is deduced from Fi−1 (2 ≤ i ≤ n) using the set of axioms and the rules of inference. A formula F for which there exists a formal proof is called a theorem.

Let us suppose that the requirements R of a design problem and the design D itself are both representable within the common framework of a formal system. In that case the problem of demonstrating that D satisfies R – that there is a fit between D and R – can be addressed by the designer formally proving the assertion ‘D satisfies R’. The latter assertion becomes, in effect, a theorem.

The notion of treating designs as formal entities so that one may prove (or verify) their correctness with respect to a requirements set is at the heart of the formal design (FD) paradigm. This paradigm originated some two decades ago in seminal papers by Floyd (1967) and Hoare (1969) which together laid the foundations for proving the correctness of programs.