NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR

Copyright Notice | |

The following manuscript | |

EWD 576 On subgoal induction | |

is held in copyright by Springer-Verlag New York. | |

The manuscript was published as pages 223–224 of | |

Edsger W. Dijkstra, Selected Writings on Computing: A Personal Perspective, | |

Springer-Verlag, 1982. ISBN 0–387–90652–5. | |

Reproduced with permission from Springer-Verlag New York. | |

Any further reproduction is strictly prohibited. |

**On subgoal induction**.

In [1] I encountered “subgoal induction” as a technique for proving partial correctness. It was applied to a program S that I would write down as

S : x:= f(x0); | ||

do B(x) → x:= g(x) od; | ||

x:= h(x) . |

{P(x0)} S {R(x0, x)} | (1) |

(A x: (non B(x)) ⇒ Q(x, z)) | (2) | |

(A x, z: (Q(g(x), z) and B(x) ⇒ Q(x, z)) | (3) | |

(A x, z: (P(x) and Q(f(x), z)) ⇒ R(x, z)) | (4) |

My general inclination when I encounter such formulae —particularly when I encounter them in a report that is really dealing with something else— is to skim them, assuming that they are no more than variations on an old theme. Formula (3), however, attracted my attention, because, if P’(x) is the invariant relation for the repetitive construct, we have to prove —see [2]—

(P’(x) and B(x) ⇒ P’(g(x)) | (5) |

In terms of a relation Q satisfying (2), (3), and (4), we can take as our invariant relation

P’(x): (A z: Q(x, z) ⇒ Q(f(x0), z)) | (6) |

((A z: Q(x, z) ⇒ Q(f(x0), z)) and B(x)) ⇒
((A z: Q(g(x), z) ⇒ Q(f(x0), z)) | (7) |

Finally we have to prove that

(P’(x) and non B(x)) ⇒ wp(“x:= h(x)”. R(x0, x)) | (8) |

(A z: Q(x, z) ⇒ Q(f(x0), z)) and Q(x, h(x)) |

Q(f(x0), h(x)) . |

R(x0, h(x)) |

Thus we have established that —as was to be expected— subgoal induction is indeed the next variation on an old theme.

The analysis described above was carried through together with C.S. Scholten.

Plataanstraat 5 | prof.dr.Edsger W.Dijkstra |

NL-4565 NUENEN | Burroughs Research Fellow |

The Netherlands |

[1] Is “sometime” sometimes better than “always”? Intermittent assertions in
proving program correctness, by Zohar Manna and Richard Waldinger, STAN-C5-76-558

[2] Guarded Commands, Nondeterminacy and Formal Derivation of Programs, by
Edsger W.Dijkstra, Comm.ACM 13, 3 (Aug.1975) 453 - 457.

Transcribed by Martin P.M. van der Burgt

Last revision