Ten years of Hoare's logic: A survey— part II: Nondeterminism

AbstractA survey of various results concerning the use of Hoare's logic in proving correctness of nondeterministic programs is presented. Various proof systems together with the example proofs are given and the corresponding soundness and completeness proofs of the systems are discussed. Programs allowing bounded and countable nondeterminism are studied. Proof systems deal with partial and total correctness, freedom of failure and the issue of fairness. The paper is a continuation of Part I by Apt (1981), where various results concerning Hoare's approach to proving correctness of sequential programs are presented