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.