# Partial and total correctness as greatest and least fixpoints

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 $\rightarrow$ between configurations. Configurations comprise a command $C$ and a state $\sigma$. Given an initial configuration $(C_0,\sigma_0)$, we can produce a transition system corresponding to all the possible computations that can arise.

A simple one is as follows:

$\begin{array}{c}(\texttt{x++} \parallel \texttt{y++},\{{\tt x}\mapsto 0,{\tt y}\mapsto 2\}) \\\swarrow \hspace{40pt} \searrow \\({\tt skip} \parallel \texttt{y++},\{{\tt x}\mapsto 1,{\tt y}\mapsto 2\}) \qquad \qquad (\texttt{x++} \parallel {\tt skip},\{{\tt x}\mapsto 0,{\tt y}\mapsto 3\}) \\\searrow \hspace{40pt} \swarrow \\({\tt skip}\parallel {\tt skip},\{{\tt x}\mapsto 1,{\tt y}\mapsto 3\}) \\ \downarrow \\ ({\tt skip},\{{\tt x}\mapsto 1,{\tt y}\mapsto 3\})\end{array}$

We can use modal-μ calculus to describe such transition systems. We shall consider modal-μ assertions with the following, slightly reduced, syntax:

$p ::= S \mid \top \mid \bot \mid p \Rightarrow p \mid p \wedge p \mid \square p \mid \lozenge p \mid \mu X\ldotp p \mid \nu X\ldotp p \mid X$

where $S$ is a set of configurations and $\mu X\ldotp p$ and $\nu X\ldotp p$ are the least and greatest assertions such that $X=p$, where $p$ contains $X$. The satisfaction relation $(C,\sigma) \models p$ is defined as follows:

$\begin{array}{lcl}(C,\sigma)\models S & \Leftrightarrow & (C,\sigma)\in S \\(C,\sigma)\models\top & \Leftrightarrow & \mathit{true} \\(C,\sigma)\models\bot & \Leftrightarrow & \mathit{false} \\(C,\sigma)\models p_1\Rightarrow p_2 & \Leftrightarrow & (C,\sigma)\models p_1 \Rightarrow (C,\sigma)\models p_2 \\(C,\sigma)\models p_1\wedge p_2 & \Leftrightarrow & (C,\sigma)\models p_1 \wedge (C,\sigma)\models p_2 \\(C,\sigma)\models\square p & \Leftrightarrow & \forall C',\sigma'\ldotp (C,\sigma)\rightarrow (C',\sigma') \Rightarrow (C',\sigma')\models p \\(C,\sigma)\models\lozenge p & \Leftrightarrow & \exists C',\sigma'\ldotp (C,\sigma)\rightarrow (C',\sigma') \wedge (C',\sigma')\models p \\(C,\sigma)\models \mu X\ldotp p & \Leftrightarrow & (C,\sigma)\in \bigcap\{S\mid p[S/X] \subseteq S\} \\(C,\sigma)\models \nu X\ldotp p & \Leftrightarrow & (C,\sigma)\in \bigcup\{S\mid S \subseteq p[S/X]\}\end{array}$

Let $P$ and $Q$ range over sets of states. Understand $(C,P)$ as a shorthand for $\{(C,\sigma)\mid \sigma\in P\}$, and let $(C,P)\models p$ mean $\forall\sigma\in P\ldotp (C,\sigma)\models p$.

Definition (Termination). A configuration $(C,\sigma)$ is stuck if no further reductions are possible. Moreover, the configuration is terminal when $C={\tt skip}$.

Definition (Partial correctness). $\{P\}\,C\,\{Q\}$ means that whenever $C$ is executed from an initial state in $P$, then in every terminal configuration it reaches, the state is in $Q$.

Definition (Total correctness). $[P]\,C\,[Q]$ means that whenever $C$ is executed from an initial state in $P$, then it reaches a terminal configuration, and in every terminal configuration it reaches, the state is in $Q$.

Conjecture. Partial correctness and total correctness are characterised by the following modal-μ assertions.

$\displaystyle \begin{array}{rcl} \{P\}\,C\,\{Q\} & \Leftrightarrow & (C,P) \models \nu X\ldotp \square X \wedge (\square\bot \Rightarrow ({\tt skip},Q)) \\ \vspace{0pt}[P]\,C\,[Q] & \Leftrightarrow & (C,P) \models \mu X\ldotp \square X \wedge (\square\bot \Rightarrow ({\tt skip},Q)) \end{array}$

Proof. To do.