Annabelle McIver and Carroll Morgan
Abstract:
Recent work in sequential program semantics has produced both an operational [4] and an axiomatic [13,17] treatment of total correctness for probabilistic demonic programs, extending Kozen's original work [9,10] that did not include demonic nondeterminism.
For practical applications however (eg. combining loop invariants with termination constraints) it is important to retain the traditional distinction between partial and total correctness. Jones [6] defines probabilistic partial correctness for probabilistic, but again not demonic programs.
In this paper we combine all the above, giving an operational and axiomatic framework for both partial and total correctness of probabilistic and demonic sequential programs; among other things that provides the theory to support practical reasoning about probabilistic demonic loops [11].