Correctness of the Algol Procedure Askforhand

Abstract

Reasons are given to justify the writing of this particular proof of correctness. They include (i) illustration of some new techniques of proof, (ii) experimentation with a method of presenting a proof and (iii) presentation of an example of a successful proof to encourage more such proofs of other programs. The specific example is an Algol procedure ASKFORHAND which is supposed to read a bridge hand from a teletype. That task is defined and a proof is given that the procedure properly performs this task.