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:
-
The algebras are partial, i.e. terms are not always defined.
-
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:
-
the assertions extend the booleans, and are 3-valued
(including the undefined value);
-
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.