Structural Induction

Discharging the proof obligations for algebraic specifications usually involves structural induction and there is no doubt that the proofs, even for small specifications, can be cumbersome. The aim of the rest of this chapter therefore is to inform reader how we would expect them to use these formal ideas and techniques. We would not expect them to prove everything formally, but to understand the principles involved in discharging the proof obligations. This should give a better understanding of the nature of the algebraic approach itself.

To keep the discussion as simple as possible, we will use the example of the specification Stack of Fig. 9.7 for an unbounded stack of natural numbers and prove that

(1) the collection of reduced expressions constitutes a set of canonical forms

(2) the specification is sufficiently complete

The formal reasoning used to prove these properties is based on structural induction, (also known as data type induction) and the arguments used can be applied similarly to prove corresponding properties for the specifications of the previous chapters. Structural induction is an extension of one of the classical proof techniques in mathematics known as mathematical induction. This idea was introduced at the end of chapter 2 and used informally in chapter 5 where the technique was applied to prove that an explicit specification satisfied an implicit one. The idea of structural induction is not always immediately accessible so we use the example of the stack to ease the analysis and give the reader confidence with the approach. The analysis scales up for larger examples without too much difficulty apart from the increased notation involved.

Structural induction is similar to the principle of mathematical induction over the integers. In the case of algebraic specifications, in order to prove that some property (predicate) P holds for all values of the data type, we have to demonstrate that the property is valid for all syntactically legal applications of the operations which produce values of the data type.

Suppose the specification of an abstract data type T has $\nu$ constructor operations C₁, C₂, $\dots$, $C_{\nu}$ where the first m of them are nullary operations (constant values). Furthermore let t_n denote a well-formed term formed from a syntactically legal composition (application) of n of these operations, so that $t_n = C_{t_1}C_{t_2} \dots C_{t_n}$ where n denotes the length of the expression t_n. For brevity of notation, we have omitted the other arguments of the constructors.

The principle of structural induction can be informally stated as follows :

(a) if we can establish the truth of P(C_i) for all nullary operations C_i where $1 \le i \le m$ and $m \le \nu$ (the base case)

(b) and that the truth of P for the term t_n implies the truth of P for all terms C_jt_n where C_jt_n is the term of length (n+1) obtained by the syntactically legal application of the constructor operation C_j to the term t_n

(c) then we can infer the truth of P for all values of the data type.

With structural induction, the base case which must be established is to demonstrate that P is true for all nullary constructor operations.

Basically, since the data values t of an abstract data type T are only modified to other values of type t by constructor operations, they must have attained their values as a result of a finite sequence of applications of these constructors, with the first operation creating a new instance of the data type (init and new in the case of the stack and queue respectively). The truth of some property P about the data type can then be inferred as a direct consequence of induction on the length of the sequence of operation applications.

There is a parallel here with proving ``valid'' output states in VDM, described in chapter 5. The ``property'' P in this case is VDM's data type invariant (dti) and the ``constructors'' C_i ( $1 \le i \le \nu$) are VDM operations which change the state.