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.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s