An Exercise in Program Explanation
An algorithm tha t computes the set of prime numbers less than or equal to some given n _ 2 is developed and explained in this paper. The algorithm employs a variation of the sieve technique; however, every nonprime is generated and removed precisely once from the set, resulting in an algorithm with running time linear in n. This efficiency is achieved at the expense of maintaining a more complex data structure and assuming tha t multiplication (of positive integers smaller than n) requires unit time. The algorithm is simpler to explain and prove than a linear algorithm appearing in [1]. The purpose of this note is to show how a combinat ion of program-proving ideas and stepwise refinement can be used to describe and explain an algori thm completely. The explanation is given by first postulating a suitable invariant. Hypothesizing an invariant is one of the most creative tasks in program construction; however, program construction becomes almost purely mechanical given a suitable invariant. The explanation given here is adequate for a reader to construct his own formal proof. For this problem Pri tchard [4] reports an asymptotical ly sublinear algorithm which uses no multiplication.