© 1972 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Proof of a structured program: The sieve of Eratosthenes
Department of Computer Science, The Queen's University of Belfast, Belfast, UK
This paper illustrates a method of constructing a program together with its proof. By structuring the program at two levels of abstraction, the proof of the more abstract algorithm may be completely separated from the proof of the concrete representation. In this way, the overall complexity of the proof is kept within more reasonable bounds.
Received March 1972.
* Department of Computer Science, The Queen's University of Belfast, Belfast BT7 1NN, Northern Ireland