Likang Zhu:   MSc, Sept. 2003.
Hoare Logics for Programming Languages with Partial Functions and Non-Deterministic Choice.

Abstract.   We develop Hoare logics for total correctness for a program language, extending the While language, over abstract many-sorted algebras, with the following features:
  1. The algebras are partial, i.e. terms are not always defined.
  2. The language includes a non-deterministic 'choice' construct

    choose z : b

    where z has type nat, and b is a boolean term, and execution diverges if there is no such z.
This language is important in the study of computation on topological partial algebras.

We develop two different logics for the assertion language, to deal with undefined truth values:

  1. the assertions extend the booleans, and are 3-valued (including the undefined value);
  2. the assertions are disjoint from the booleans, and are 2-valued (without undefinedness).

These lead to two distinct (but similar) Hoare logics.

Our Hoare proof rule for the 'choose' construct seems to be original:

{Exists z : b} choose z : b {b}

We prove soundness for the Hoare system in both logics, and apply it to a case study: solving a linear system of equations by Gaussian elimination.