Program proving: Coroutines

Summary Proof methods adequate for a wide range of computer programs have been given in 1–6]. This paper develops a method suitable for programs which incorporate coroutines. The implementation of coroutines described follows closely that given in SIMULA 7, 8], a language in which such features may be used to great advantage. Proof rules for establishing the correctness of coroutines are given and the method is illustrated by the proof of a useful program for histogram compilation.