This short note explains how partial and total correctness triples can be characterised as the greatest and least fixpoints, respectively, of the same function.
Suppose we have a small-step transition relation between configurations. Configurations comprise a command and a state . Given an initial configuration , we can produce a transition system corresponding to all the possible computations that can arise.
A simple one is as follows:
We can use modal-μ calculus to describe such transition systems. We shall consider modal-μ assertions with the following, slightly reduced, syntax:
where is a set of configurations and and are the least and greatest assertions such that , where contains . The satisfaction relation is defined as follows:
Let and range over sets of states. Understand as a shorthand for , and let mean .
Definition (Termination). A configuration is stuck if no further reductions are possible. Moreover, the configuration is terminal when .
Definition (Partial correctness). means that whenever is executed from an initial state in , then in every terminal configuration it reaches, the state is in .
Definition (Total correctness). means that whenever is executed from an initial state in , then it reaches a terminal configuration, and in every terminal configuration it reaches, the state is in .
Conjecture. Partial correctness and total correctness are characterised by the following modal-μ assertions.
Proof. To do.