A note on “tail invariants”

The purpose of this note, which is mainly for the record, is to describe a phenomenon which is well-known (and has been named) in Eindhoven, but deserves to be known more widely. In addition, we might be able to offer some explanation of the phenomenon.

The archetypal problem - archetypal

$$ \left\lfloor \operatorname {c o n} X, Y; \operatorname {i n t} {X > 0 \land Y \geqslant 0 } \right. $$

$$ \therefore \text {v a r} z: \text {i n t} $$

$$ ; e x p o n e n t i a t i o n {z = X ^ {r} } $$

$$ ] ] \quad . $$

Our first solution, $\exp ,$ does not use a tail invariant.

$$ \begin{array}{l} e x p 0: \ll a r y: i n t \ ; y, z := 0, 1 {P _ {0}: 0 \leq y \leq Y \land z \geq 1 \land z = X ^ {y} } \ ; \underline {{\underline {{d o}}}} y \neq Y \rightarrow y, z := y + 1, X \cdot z \underline {{\underline {{o d}}}} \ {P O \wedge y = Y, h e n c e } \ ] \left{z = X ^ {Y} \right} \ \end{array} $$

Our second solution, $\exp 1$ ,does use what is known as a tail invariant.

$$ \begin{array}{l} e x p 1: \left\lfloor \begin{array}{l} \text {v a r y}: \end{array} \right. \mathrm {i n t} \ ; y, z := Y, 1 {P _ {1}: 0 \leq y \leq Y \land 2 \geq 1 \land z \cdot X ^ {y} = X ^ {Y} } \ ; \underline {{\underline {{d o}}}} y \neq 0 \rightarrow y, z := y - 1, X \cdot z \underline {{\underline {{o d d}}}} \ \begin{array}{r l} & {{\mathrm {P r} \wedge y = 0, \mathrm {h e n c e} }} \ & {{\mathrm {Z} = \overline {{X ^ {\prime}}} }} \end{array} \ \end{array} $$

In the repetition we used in both programs the property of exponentiation - the "step"

$$ X ^ {y + 1} = X \cdot X ^ {y}; $$

in both programs we used the property of

$$ X ^ {0} = 1, $$

but the difference is where it was used. In $\exp 0$ ,the base was used to justify the initializatio $\left( {ofy}\right)$ -while the implication of the postcondition by P17B requires only Leibniz's Principle. In $\exp 1$ , the justification of the initialization requires Leibniz's Principle but no properties of expon- nentiation: the base is needed for the final implication of the postcondition.

The general experience is that the tail invariant is to be preferred : its use gives rise to the nicer derivations or the nicer programs or both. The explanation has probably many facets, one of them possibly

being that the mathematical setting of ${exp1}$ is slightly richer than that of ${exp0}$ ,in which - in contrast to ${exp1} -$ no use is made of the fact that 1 is the neutral element of the multiplication. More important is that the tail invariant gives greater flexibility.

In both programs - with ${XY}$ in the invariant - z's final value ${X}^{Y}$ is primarily treated as a function of $Y$ . That $Z$ has its final value ${X}^{Y}$ has to be concluded from " $P \land {PB}$ ".

In expo, Y does not occur in the invariant Po, therefore Y has to occur in the guard. In expl, it is the other way round: Y occurs in invariant P but not in the guard. And here you see a major difference: in the invariant we can allow Y to occur via a nonprimitive subexpression like $X^Y$ , but doing so in the guard would be beg- ging the question.

(We reject

$$ \begin{array}{l} e x p 2: \left\lceil z := 1 \quad {P _ {2}: 1 \leq z \leq X ^ {r} \right\rceil \ ; \underline {{d o}} z \neq X ^ {\gamma} \rightarrow z := z + 1 \quad o d \ ] 1 {z = X ^ {Y} } \ \end{array} $$

for obvious reasons.)

The greater flexibility of the tail invariant immediately manifests itself when we consider the value to be computed as a function of both $X$ and $Y$ :

$$ \begin{array}{l} e x p 3: \llbracket \operatorname {v a r} x, y: \mathrm {i n t}; x, y, z := X, Y, i \ {P _ {3}: 1 \leq x \wedge 0 \leq y \leq Y \wedge 1 \leq z \wedge X ^ {Y} = 2 \cdot x ^ {y} } \ \therefore \underline {{d o}} y \neq 0 \rightarrow \ i f o d d. y \rightarrow y, z := y - 1, x \cdot z \ f r e v e n. y \rightarrow x, y := x \cdot x, y / 2 \ \left{ \begin{array}{l} p _ {i} \ F \end{array} \right} \ \operatorname {o d} \left{P _ {3} \wedge y = 0, h e n c e \right} \ \left{ \begin{array}{l} z = X ^ {Y} \end{array} \right}, \ \end{array} $$

in which we could exploit ${x}^{2 \cdot n} = {\left( {x}^{2}\right) }^{n}$ to turn a linear algorithm into a logarithmic one. For the "base" it exploits in the final justification of the postcondition that ${x}^{0} = 1$ (regardless of how high a power of

It is the last observation that pinpoints the problem with $\exp 0$ ,when we would like to introduce the variable $x$ there too. In order to establish -analogously to $P_0$

$$ z = x ^ {y} $$

we could, so to speak, initialize

$$ x, y, z := ?, 0, 1 $$

where any positive "?" would do. It is hard to exploit that freedom in a constructive fashion, and for the time being it seems a wise precaution to become very suspicious when confronted with an initialization in which the value of one of the variables is irrelevant.

It all strongly suggests to shape our calculations as computations of recursively defined functions and to justify that initializations establish invariants by an appeal to Leibniz's Principle and not to properties of the functions to be computed. We note that (pure) functional programming languages go a long way towards syntactic enforcement of this discipline.

Austin, 1 October 1993

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA