Operational Annotations

A new method for sequential program verification

Paul C. Attie
School of Computer and Cyber Sciences
Augusta University

I present a new method for specifying and verifying the partial correctness of
sequential programs. The key observation is that, in Hoare logic, assertions
are used as selectors of states: an assertion specifies the set of program
states which satisfy the assertion. Hence, the usual meaning of the partial
correctness Hoare triple $\\{f\\}\,P\,\\{g\\}$: if execution is started in
_any of the states that satisfy assertion $f$_, then, upon termination, the
resulting state will be _some state that satisfies assertion $g$_. There are
of course other ways to specify a set of states. I propose to replace
assertions by terminating programs: a program $\alpha$ specifies a set of
states as follows: we start $\alpha$ in any state whatsoever, and all the
states that $\alpha$ may terminate in constitute the specified set. I call
this set the _post-states_ of $\alpha$. I introduce the _operational triple_
$[\alpha]\,P\,[\beta]$ to mean: if execution of $P$ is started in any post-
state of $\alpha$, then upon termination, the resulting state will be some
post-state of $\beta$. Here, $\alpha$ is the _pre-program_ , and plays the
role of a pre-condition, and $\beta$ is the _post-program_ , and plays the
role of a post-condition.

Keywords: Program verification, Hoare logic

##  1 Introduction

I present a system for verifying partial correctness of deterministic
sequential programs. In contrast to Floyd-Hoare logic [5, 9], my system does
not use pre-conditions and post-conditions, but rather pre-programs and post-
programs. An assertion is essentially a means for defining a set of states:
those for which the assertion evaluates to true. Hence the usual Hoare triple
$\\{f\\}\,P\,\\{g\\}$ means that if execution of $P$ is started in _any of the
states that satisfy assertion $f$_, then, upon termination of $P$, the
resulting state will be _some state that satisfies assertion $g$_.

Another method of defining a set of states is with a program $\alpha$ which
starts execution in any state, i.e., with precondition $\mathit{true}$. The
set of states in which $\alpha$ terminates (taken over all possible starting
states) constitues the set of states that $\alpha$ defines. I call these the
post-states of $\alpha$.

I introduce the operational triple $[\alpha]\,P\,[\beta]$, in which $\alpha$
and $\beta$ are terminating sequential programs, and $P$ is the sequential
program that is being verified. $\alpha$ is the _pre-program_ and $\beta$ is
the _post-program_. The meaning of $[\alpha]\,P\,[\beta]$ is as follows.
Consider executions of $\alpha$ that start in any state (i.e., any assignment
of values to the variables). From the final state of all such executions, $P$
is executed. Let $\varphi$ be the set of resulting final states. That is,
$\varphi$ results from executing $P$ from any post-state of $\alpha$. Also,
let $\psi$ be the set of post-states of $\beta$, i.e., the set of states that
result from executing $\beta$ starting in any state. Then,
$[\alpha]\,P\,[\beta]$ is defined to mean $\varphi\subseteq\psi$. That is, the
post-states of $\alpha;P$ are a subset of the post-states of $\beta$.

The advantages of my approach are as follows. Since the pre-program $\alpha$
and the program $P$ are constituted from the same elements, namely program
statements, it is easy to “trade” between the two, i.e., to move a statement
from the program to the pre-program and vice-versa. This tactic is put to good
use in in deriving programs from operational specifications, and is
illustrated in the examples given in this paper. Since the pre-program
$\alpha$ and post-program $\beta$ are not actually executed, then can be
written without concern for efficiency. In fact, they can refer to any well
defined expression, e.g., $\delta[t]$ for the shortest path distance from a
designated source $s$ to node $t$.

##  2 Technical preliminaries

###  2.1 Syntax of the programming language

I use a basic programming language consisting of standard primitive types
(integers, boolean etc), arrays, and reference types, assignments, if
statements, while loops, for loops, procedure definition and invocation, class
definition, object creation and referencing. The syntax that I use is given by
the BNF grammar in Table 1. I omit the definitions for $\mathit{Id}$
(identifier), $\mathit{Num}$ (numeral), $\mathit{Obj}$ (object reference), as
these are primarily lexical in nature. I assume as given the grammar classes
$\mathit{Primitive}$ for primitive types, and $\mathit{Reference}$ for
reference types, i.e., my syntax is parametrized on these definitions.

My syntax is standard and self-explanatory. I also use $[]$ to denote non-
deterministic choice between two commands [8]. For integers $i,j$ with
$i\leqslant j$, I use $x\colonequals[i:j]$ as syntactic sugar for
$x\colonequals i\mbox{[]}\cdots\mbox{[]}x\colonequals j$, i.e., a random
assignment of a value in $i,\ldots,j$ to $x$. This plays the role of the range
assertion $i\leqslant x\leqslant j$ in Hoare logic. I use $\mathit{tt}$ for
true, and $\mathit{ff}$ for false.

In the sequel, when I use the term “program”; I will mean a statement
$(\mathit{Stat})$ written in the language of Table 1. I use $\mathit{tt}$ for
true, and $\mathit{ff}$ for false.

$\mathit{Type}::=\mathit{Primitive}\ \ |\ \ \mathit{Reference}\ \ |\ \
\mathit{void}$
$\mathit{Array}::=\mathit{Id}[\mathit{Expr}]$ //array element — boolean or
integer valued
$\mathit{Bool}::=\mathit{tt}\ |\ \mathit{ff}\ |\ \mathit{Id}\ |\
\mathit{Bool}\land\mathit{Bool}\ |\ \mathit{Bool}\lor\mathit{Bool}\ |\
\neg\mathit{Bool}\ |\ \mathit{Arith}<\mathit{Arith}\ |\
\mathit{Arith}=\mathit{Arith}$ //Boolean expression
$\mathit{Arith}::=\mathit{Id}\ |\ \mathit{Num}\ |\ \mathit{Arith}\ |\
\mathit{Arith}+\mathit{Arith}\ |\ \mathit{Arith}*\mathit{Arith}\ |\
\mathit{Arith}-\mathit{Arith}\ |\ -\mathit{Arith}$ //integer-valued arithmetic
expression
$\mathit{Expr}::=\mathit{Bool}\ |\ \mathit{Arith}\ |\ \mathit{Obj}$
//expression
$\mathit{Var\\_Decl}::=\mathit{Type}\ \mathit{Id}$
$\mathit{Var\\_List}::=\mathit{Var\\_Decl}\ |\
\mathit{Var\\_Decl},\mathit{Var\\_List}$
$\mathit{Expr\\_List}::=\mathit{Expr}\ |\ \mathit{Expr},\mathit{Expr\\_List}$
$\mathit{Proc\\_Def}::=\mathit{Type}\ \mathit{Id}(\mathit{Var\\_List})\
\mathit{Stat}$
$\mathit{Proc\\_Call}::=\mathit{Id}(\mathit{Parameter\\_List})\ |\
\mathit{Id}\colonequals\mathit{Id}(\mathit{Parameter\\_List})$
$\mathit{Proc\\_List}::=\mathit{Proc\\_Def}\ |\ \mathit{Proc\\_Def}\
\mathit{Proc\\_List}$
$\mathit{ClassDef}::=\mathit{Class}\ \mathit{Id}\ \\{\mathit{Var\\_List};\
\mathit{Proc\\_List}\\}$
$\mathit{Object\\_Create}::=\mathit{Type}\ \mathit{Obj}:=new\
\mathit{Id}(\mathit{Parameter\\_List})$ //object creation
$\mathit{Assign}::=\mathit{Id}\colonequals\mathit{Expr}\ |\
\mathit{Array}\colonequals\mathit{Expr}\ |\
\mathit{Obj}\colonequals\mathit{Expr}\ |\
\mathit{Obj}.\mathit{Id}\colonequals\mathit{Expr}$
$\mathit{Selection}::={\boldsymbol{\mathit{if}}}\ (\mathit{Bool})\
{\boldsymbol{\mathit{then}}}\ \mathit{Stat}\ {\boldsymbol{\mathit{else}}}\
\mathit{Stat}\ {\boldsymbol{\mathit{fi}}}\ |\ {\boldsymbol{\mathit{if}}}\
(\mathit{Bool})\ {\boldsymbol{\mathit{then}}}\ \mathit{Stat}\
{\boldsymbol{\mathit{fi}}}$
$\mathit{Ret}::=\mathit{Return}\ |\ \mathit{Return}(\mathit{Expr})$
$\mathit{Iteration}::={\boldsymbol{\mathit{while}}}\ (\mathit{Bool})\
\mathit{Stat}\ {\boldsymbol{\mathit{elihw}}}\ |\ {\boldsymbol{\mathit{for}}}\
(\mathit{Id}=\mathit{Arith}\ {\boldsymbol{\mathit{to}}}\ \mathit{Arith})\
\mathit{Stat}{\boldsymbol{\mathit{rof}}}$
$\mathit{Stat}::=\mathit{skip}\ |\ \mathit{Stat};\mathit{Stat}\ |\
\mathit{Stat}\,\mbox{[]}\,\mathit{Stat}\ |\ \mathit{Assign}\ |\
\mathit{Selection}\ |\ \mathit{Iteration}\ |\ \mathit{Proc\\_Call}\ |\
\mathit{Object\\_Create}$ //Statement

Table 1: Syntax of the programming language

###  2.2 Semantics of the programming language

I assume the usual semantics for reference types: object identifiers are
pointers to the object, and the identity of an object is given by its location
in memory, so that two objects are identical iff they occupy the same memory.
Parameter passing is by value, but as usual a passed array/object reference
allows the called procedure to manipulate the original array/object. My proof
method relies on (1) the axioms and inference rules introduced in this paper,
and (2) an underlying method for establishing program equivalence. Any
semantics in which the above are valid can be used. For concreteness, I assume
a standard small-step (SOS) operational semantics [23, 25].

An execution of program $P$ is a finite sequence $s_{0},s_{1},\ldots,s_{n}$ of
states such that (1) $s_{i}$ results from a single small step of $P$ in state
$s_{i-1}$, for all $i\in 1,\ldots,n$, (2) $s_{0}$ is an initial state of $P$,
and (3) $s_{n}$ is a final (terminating) state of $P$. A behavior of program
$P$ is a pair of states $(s,t)$ such that (1) $s_{0},s_{1},\ldots,s_{n}$ is an
execution of $P$, $s=s_{0}$, and $t=s_{n}$. Write $\\{|P|\\}$ for the set of
behaviors of $P$.

###  2.3 Hoare Logic

I assume standard first-order logic, with the standard model of arithmetic and
standard Tarskian semantics. Hence I take the notation $s\models f$, where $s$
is a state and $f$ is a formula, to have the usual meaning.

I use the standard notation for Hoare-logic partial correctness:
$\\{f\\}\,P\,\\{g\\}$ means that if execution of program $P$ starts from a
state satisfying formula $f$, then, if $P$ terminates, the resulting final
state will satisfy formula $g$. That is, for all $(s,t)\in\\{|P|\\}$, if
$s\models f$ then $t\models g$.

##  3 Operational annotations

I use a terminating program to specify a set of states. There is no constraint
on the initial states, and the set of all possible final states is specified.
If any initialization of variables is required, this must be done explicitly
by the program.

######  Definition 1 (Post-state set)

Let $P$ be a program. Then

$\mathit{post}(P)\triangleq\left\\{t\ |\
(\exists\,s:(s,t)\in\\{|P|\\})\right\\}$

That is, $\mathit{post}(P)$ is the set of all possible final states of $P$,
given any initial state. If one increases the set of states in which a program
can start execution, then the set of states in which the program terminates is
also possibly increased, and is certainly not decreased. That is, the set of
post-states is monotonic in the set of pre-states. Since prefixing a program
$\alpha$ with another program $\gamma$ simply restricts the states in which
$\alpha$ starts execution, I have the following.

###### Proposition 1

$\gamma;\alpha\preceq\alpha$.

Proof. Let $s\in\mathit{post}(\gamma;\alpha)$. Then, there is some state $u$
such that $u\in\mathit{post}(\gamma)$ and $(u,s)\in\\{|\alpha|\\}$. Hence
$s\in\mathit{post}(\alpha)$. So
$\mathit{post}(\gamma;\alpha)\subseteq\mathit{post}(\alpha)$, from which
$\gamma;\alpha\preceq\alpha$ follows. $\Box$

The central definition of the paper is that of _operational triple_
$[\alpha]\,P\,[\beta]$:

######  Definition 2 (Operational triple)

Let $\alpha$, $P$, and $\beta$ be programs. Then

$[\alpha]\,P\,[\beta]\;\triangleq\;\mathit{post}(\alpha;P)\subseteq\mathit{post}(\beta).$

###  3.1 Program Ordering and Equivalence

The next section presents a deductive system for establishing validity of
operational triples. The rules of inference use three kinds of hypotheses: (1)
operational triples (over “substatements” as usual), and (2) program ordering
assertions $P\preceq Q$, and (3) program equivalence assertions $P\equiv Q$.

######  Definition 3 (Program ordering)

$P\preceq Q\triangleq\mathit{post}(P)\subseteq\mathit{post}(Q)$.

Here $P$ is “stronger” than $Q$ since it has fewer post-states (w.r.t., the
pre-condition $\mathit{tt}$, i.e., all possible pre-states), and so $P$
produces an output which satisfies, in general, more constraints than the
output of $Q$. Note that this is _not_ the same as the usual program
refinement relation, since the mapping from pre-states to post-states induced
by the execution of $P$ is not considered. Also, the “direction” of the
inclusion relation is reversed w.r.t. the usual refinement ordering, where we
write $Q\sqsubseteq P$ to denote that “$P$ refines $Q$”, i.e., $P$ satisfies
more specifications than $Q$. This is in keeping with the importance of the
post-state set in the sequel. Note that, by Definition 3 ,
$[\alpha]\,P\,[\beta]\;\triangleq\;{\alpha;P}\preceq\mathit{post}(\beta).$

######  Definition 4 (Program equivalence, $\equiv$)

Programs $P$ and $Q$ are _equivalent_ iff they have the same behaviors$:$
$P\equiv Q\triangleq\\{|P|\\}=\\{|Q|\\}$.

That is, I take as program equivalence the equality of program behaviors. Note
that equivalence is _not_ ordering in both directions. This discrepancy is
because ordering is used for weakening/strengthening laws (and so post-state
inclusion is sufficient) while equivalence is used for substitution, and so,
for programs at least, equality of behaviors is needed.

Any method for establishing program ordering and equivalence is sufficient for
my needs. The ordering and equivalence proofs in this paper were informal, and
based on obvious concepts such as the commutativity of assignment statements
that modify different variables/objects.

Works that provide proof systems for program equivalence include [2, 21, 12,
3, 22]. Some of these are mechanized, and some use bisimulation and circular
reasoning. I will look into using these works for formally establishing
program equivalence hypotheses needed in my examples (which are then akin to
Hoare logic verification conditions), and to adapting these systems to
establish program ordering, e.g., replace bisimulation by simulation.

##  4 A deductive system for operational annotations

$[\alpha]\,P\,[\alpha;P]$ (Sequence Axiom)

$[\mathit{skip}]\,P\,[P]$ (Empty Pre-program)

$[\alpha]\,\mathit{skip}\,[\alpha]$ (Empty Program)

$[\alpha]\,P1;P2\,[\beta]$ iff $[\alpha;P1]\,P2\,[\beta]$ (Trading)

$[\alpha]\,P\,[\beta]$ $[\alpha]\,P;\gamma\,[\beta;\gamma]$ (Append)

$\alpha$ ≡$\alpha$’ $P$ ≡$P$’ $\beta$ ≡$\beta$’ $[\alpha]\,P\,[\beta]$
$[\alpha^{\prime}]\,P^{\prime}\,[\beta^{\prime}]$ (Substitution)

$\alpha$ ⪯$\alpha$’ $[\alpha^{\prime}]\,P\,[\beta]$ $[\alpha]\,P\,[\beta]$
(Pre-program Strengthening)

$[\alpha]\,P\,[\beta^{\prime}]$ $\beta$’ ⪯$\beta$ $[\alpha]\,P\,[\beta]$
(Post-program Weakening)

$[\alpha]\,P1\,[\beta]$ $[\beta]\,P2\,[\gamma]$ $[\alpha]\,P1;P2\,[\gamma]$
(Sequential Composition)

$[\alpha^{\prime}]\,P\,[\alpha]$ $[\alpha]\,{\boldsymbol{\mathit{while}}}\
(B)\ P\ {\boldsymbol{\mathit{elihw}}}\,[\beta]$ $\alpha$’ ≅($\alpha$, B),
$\beta$ ≅($\alpha$, ¬B) (While)

$[\alpha^{\prime}]\,P\,[\gamma;\alpha]$
$[\alpha]\,{\boldsymbol{\mathit{while}}}\ (B)\ P\
{\boldsymbol{\mathit{elihw}}}\,[\beta]$ $\alpha$’ ≅($\alpha$, B), $\beta$
≅($\alpha$, ¬B) (While Consequence)

$[\alpha^{\prime}]\,P1\,[\beta]$ $[\alpha^{\prime\prime}]\,P2\,[\beta]$
$[\alpha]\,{\boldsymbol{\mathit{if}}}\ {B}\ {\boldsymbol{\mathit{then}}}\ P1\
{\boldsymbol{\mathit{else}}}\ P2\ {\boldsymbol{\mathit{fi}}}\,[\beta]$
$\alpha$’ ≅($\alpha$, B), $\alpha$” ≅($\alpha$, ¬B) (If)

$[\alpha^{\prime}]\,P\,[\beta]$ $\alpha$” ⪯$\beta$
$[\alpha]\,{\boldsymbol{\mathit{if}}}\ {B}\ {\boldsymbol{\mathit{then}}}\ P\
{\boldsymbol{\mathit{fi}}}\,[\beta]$ $\alpha$’ ≅($\alpha$, B), $\alpha$”
≅($\alpha$, ¬B) (One-way If)

Table 2: Axioms and rules of inference

Table 2 presents a deductive system for operational annotations. I do not
provide a rule for the ${\boldsymbol{\mathit{for}}}$ loop, since it can be
easily turned into a while. ${\boldsymbol{\mathit{for}}}$ loops quite compact,
and so are very convenient for use in pre-programs and post-programs, i.e.,
_as_ annotations. The following are informal intuition and proofs of soundness
for the axioms and inference rules.

###  4.1 Axioms

#### Sequence Axiom.

If $P$ executes after pre-program $\alpha$, the result is identical to post-
program $\alpha;P$, i.e., the sequential composition of $\alpha$ and $P$. This
gives an easy way to calculate a post-program for given pre-program and
program. The corresponding Hoare logic notion, namely the strongest
postcondition, is easy to compute (in closed form) only for straight-line
code.

###### Proposition 2

(Sequence Axiom) is valid

Proof. By Definition 2, $[\alpha]\,P\,[\alpha;P]$ is
$\mathit{post}(\alpha;P)\subseteq\mathit{post}(\alpha;P)$, which is immediate.
$\Box$

#### Empty pre-program.

Follows from (Sequence Axiom) by replacing $\alpha$ by the empty program
$\mathit{skip}$. Program $P$ is “doing all the work”, and so the resulting
post-program is also $P$. Having $\mathit{skip}$ as a pre-program is similar
to having $\mathit{tt}$ as a precondition in Hoare logic.

#### Empty Program.

Follows from (Sequence Axiom) by replacing $P$ by the empty program
$\mathit{skip}$. This is analogous to the axiom for $\mathit{skip}$ in Hoare
logic: $\\{f\\}\,\mathit{skip}\,\\{f\\}$, since $\mathit{skip}$ has no effect
on the program state.

###  4.2 Rules of Inference

#### Trading Rule.

Sequential composition is associative: $\alpha;(P1;P2)\equiv(\alpha;P1);P2$.
By Definitions 4, 1:
$\mathit{post}(\alpha;(P1;P2))=\mathit{post}((\alpha;P1);P2)$ Hence, if the
program is a sequential composition $P1;P2$, I can take $P1$ and add it to the
end of the pre-program $\alpha$. I can also go in the reverse direction, so
technically there are two rules of inference here. I will refer to both rules
as (Trading). This _seamless transfer between program and pre-program has no
analogue in Hoare logic_ , and provides a major tactic for the derivation of
programs from operational specifications.

###### Proposition 3

(Trading) is sound, that is, each side holds iff the other does.

Proof. By Definition 2, $[\alpha]\,P1;P2\,[\beta]$ is
$\mathit{post}(\alpha;P1;P2)\subseteq\mathit{post}(\beta)$, and
$[\alpha;P1]\,P2\,[\beta]$ is also
$\mathit{post}(\alpha;P1;P2)\subseteq\mathit{post}(\beta)$. Hence each holds
iff the other does. $\Box$

#### Append Rule.

Appending the same program $\gamma$ to the program and the post-program
preserves the validity of an operational triple. This is useful for appending
new code into both the program and the post-program.

###### Proposition 4

(Append) is sound, that is, if the hypothesis holds, then so does the
conclusion.

Proof. I must show $[\alpha]\,P;\gamma\,[\beta;\gamma]$, which by Definition 2
is $\mathit{post}(\alpha;P;\gamma)\subseteq\mathit{post}(\beta;\gamma)$. Let
$s\in\mathit{post}(\alpha;P;\gamma)$. Hence there is some state $t$ such that
$t\in\mathit{post}(\alpha;P)$ and $(t,s)\in\\{|\gamma|\\}$. By assumption,
$[\alpha]\,P\,[\beta]$, which by Definition 2 is
$\mathit{post}(\alpha;P)\subseteq\mathit{post}(\beta)$. Since
$t\in\mathit{post}(\alpha;P)$, I have $t\in\mathit{post}(\beta)$. Since
$(t,s)\in\\{|\gamma|\\}$, I also have $s\in\mathit{post}(\beta;\gamma)$. Since
$s$ was chosen arbitrarily, I conclude
$\mathit{post}(\alpha;P;\gamma)\subseteq\mathit{post}(\beta;\gamma)$. $\Box$

#### Substitution Rule.

Since the definition of operational annotation refers only to the behavior of
a program, it follows that one equivalent program can be replaced by another,
This rule is useful for performing equivalence-preserving transformations,
such as loop unwinding.

###### Proposition 5

(Substitution) is sound, that is, if the hypothesis holds, then so does the
conclusion.

Proof. $\alpha\equiv\alpha^{\prime}$ implies that
$\mathit{post}(\alpha)=\mathit{post}(\alpha^{\prime})$. $P\equiv P^{\prime}$
means that $\\{|P|\\}=\\{|P^{\prime}|\\}$. Hence
$\mathit{post}(\alpha;P)=\mathit{post}(\alpha^{\prime};P^{\prime})$.
$\beta\equiv\beta^{\prime}$ implies that
$\mathit{post}(\beta)=\mathit{post}(\beta^{\prime})$. Hence
$\mathit{post}(\alpha;P)\subseteq\mathit{post}(\beta)$ iff
$\mathit{post}(\alpha^{\prime};P^{\prime})\subseteq\mathit{post}(\beta^{\prime})$.
Hence $[\alpha]\,P\,[\beta]$ iff
$[\alpha^{\prime}]\,P^{\prime}\,[\beta^{\prime}]$. $\Box$

###  4.3 Rules of inference that are analogues of Hoare logic laws

I now present syntax-based rules, which are straightforward analogues of the
corresponding Hoare logic rules.

#### Pre-program strengthening.

Reducing the set of post-states of the pre-program cannot invalidate an
operational triple.

###### Proposition 6

(Pre-program Strengthening) is sound.

Proof. Let $t\in\mathit{post}(\alpha;P)$. Then there exists a state $s$ such
that $s\in\mathit{post}(\alpha)$ and $(s,t)\in\\{|P|\\}$. By assumption,
$\alpha\preceq\alpha^{\prime}$, and so
$\mathit{post}(\alpha)\subseteq\mathit{post}(\alpha^{\prime})$. Hence
$s\in\mathit{post}(\alpha^{\prime})$. From this and $(s,t)\in\\{|P|\\}$, I
conclude $t\in\mathit{post}(\alpha^{\prime};P)$. Since $t$ is arbitrarily
chosen, I have
$\mathit{post}(\alpha;P)\subseteq\mathit{post}(\alpha^{\prime};P)$. Hypothesis
$[\alpha^{\prime}]\,P\,[\beta]$ means
$\mathit{post}(\alpha^{\prime};P)\subseteq\mathit{post}(\beta)$. Hence
$\mathit{post}(\alpha;P)\subseteq\mathit{post}(\beta)$, and so
$[\alpha]\,P\,[\beta]$ by Definition 2. $\Box$

#### Post-program weakening.

Enlarging the set of post-states of the post-program cannot invalidate an
operational triple.

###### Proposition 7

(Post-program Weakening) is sound.

Proof. Hypothesis $[\alpha]\,P\,[\beta^{\prime}]$ means
$\mathit{post}(\alpha;P)\subseteq\mathit{post}(\beta^{\prime})$. Hypothesis
$\beta^{\prime}\preceq\beta$ means that
$\mathit{post}(\beta^{\prime})\subseteq\mathit{post}(\beta)$. Hence
$\mathit{post}(\alpha;P)\subseteq\mathit{post}(\beta)$, and so
$[\alpha]\,P\,[\beta]$ by Definition 2. $\Box$

#### Sequential composition.

The post-state set of $\beta$ serves as the intermediate state-set in the
execution of $P1;P2$: it characterizes the possible states after $P1$ executes
and before $P2$ executes. That is, execution of $P$ 1 starting from a post-
state of $\alpha$ yields a post-state of $\beta$. Then execution of $P$ 2
starting from a post-state of $\beta$ yields a post-state of $\gamma$.

###### Proposition 8

(Sequential Composition) is sound.

Proof. Let $t\in\mathit{post}(\alpha;P1;P2)$. Then there is some $s$ such that
$s\in\mathit{post}(\alpha;P1)$ and $(s,t)\in\\{|P2|\\}$. From hypothesis
$[\alpha]\,P1\,[\beta]$, I have
$\mathit{post}(\alpha;P1)\subseteq\mathit{post}(\beta)$. Hence
$s\in\mathit{post}(\beta)$. From this and $(s,t)\in\\{|P2|\\}$, I have
$t\in\mathit{post}(\beta;P2)$. From hypothesis $[\beta]\,P2\,[\gamma]$, I have
$\mathit{post}(\beta;P2)\subseteq\mathit{post}(\gamma)$. From this and
$t\in\mathit{post}(\beta;P2)$, I have $t\in\mathit{post}(\gamma)$. Since $t$
is chosen arbitrarily, I conclude
$\mathit{post}(\alpha;P1;P2)\subseteq\mathit{post}(\gamma)$. Hence
$[\alpha]\,P1;P2\,[\gamma]$ by Definition 2. $\Box$

#### While Rule.

Given $[\alpha]\,P\,[\alpha]$, I wish to conclude
$[\alpha]\,{\boldsymbol{\mathit{while}}}\ (B)\ P\,[\beta]$ where $\beta$ is a
“conjunction” of $\alpha$ and $\neg B$, i.e., the post-states of $\beta$ are
those that are post-states of $\alpha$, and also that satisfy assertion $\neg
B$, the negation of the looping condition. Also, I wish to weaken the
hypothesis of the rule from $[\alpha]\,P\,[\alpha]$ to
$[\alpha^{\prime}]\,P\,[\alpha]$, where $\alpha^{\prime}$ is a “conjunction”
of $\alpha$ and $B$, i.e., the post-states of $\alpha^{\prime}$ are those that
are post-states of $\alpha$ and that also satisfy assertion $B$, the looping
condition. I therefore define the “conjunction” of a program and an assertion
as follows.

######  Definition 5 (Conjunction of program and condition)

Let $\alpha^{\prime},\alpha$ be programs and $B$ a Boolean expression. Then
define

$\alpha^{\prime}\cong(\alpha,B)\triangleq\mathit{post}(\alpha^{\prime})=\mathit{post}(\alpha)\cap\left\\{s\
|\ s(B)=\mathit{tt}\right\\}.$

Note that this definition does not produce a unique result, and so is really a
relation rather than a mapping. The construction of $\alpha^{\prime}$ is not
straightforward, in general, for arbitrary assertion $B$. Fortunately, most
looping conditions are simple, typically a loop counter reaching a limit. I
therefore define the needed program $\alpha^{\prime}$ by the semantic
condition given above, and leave the problem of deriving $\alpha^{\prime}$
from $\alpha$ and $B$ to another occasion.

Given a while loop ${\boldsymbol{\mathit{while}}}\ (B)\ P\
{\boldsymbol{\mathit{elihw}}}$ and pre-program $\alpha$, let $\alpha^{\prime}$
be a program such that $\alpha^{\prime}\cong(\alpha,B)$, and let $\beta$ be a
program such that $\beta\cong(\alpha,\neg B)$. The hypothesis of the rule is:
execute $\alpha$ and restrict the set of post-states to those in which $B$
holds. That is, have $\alpha^{\prime}$ as a pre-program for the loop body $P$.
Then, after $P$ is executed, the total resulting effect must be the same as
executing just $\alpha$. So, $\alpha$ is a kind of “operational invariant”.
Given that this holds, and taking $\alpha$ as a pre-program for
${\boldsymbol{\mathit{while}}}\ (B)\ P\ {\boldsymbol{\mathit{elihw}}}$, then
upon termination, we have $\alpha$ as a post-program. On the last iteration,
$B$ is false, and the operational invariant $\alpha$ still holds. Hence I can
assert $\beta$ as a post-program for the ${\boldsymbol{\mathit{while}}}$ loop.

###### Theorem 9

(While) is sound, i.e., if the hypothesis is true, then so is the conclusion.

Proof. I establish, by induction on $i$, the following claim:

> Assume the hypothesis $[\alpha^{\prime}]\,P\,[\alpha]$, and that execution
> of the loop starts in a state $s_{0}\in\mathit{post}(\alpha)$. Then if the
> loop executes for at least $i$ iterations, the state $s_{i}$ at the end of
> the $i$’th iteration is in $\mathit{post}(\alpha)$.

Base case is for $i=0$: The state at the end of the 0’th iteration is just the
start state $s_{0}$, which is in $\mathit{post}(\alpha)$ by assumption.
Induction step for $i>0$: By the induction hypothesis,
$s_{i-1}\in\mathit{post}(\alpha)$. Now $s_{i-1}(B)=\mathit{tt}$, since
otherwise the $i$’th iteration would not have been executed. Hence
$s_{i-1}\in\mathit{post}(\alpha^{\prime})$. By the hypothesis
$[\alpha^{\prime}]\,P\,[\alpha]$, I have $s_{i}\in\mathit{post}(\alpha)$.

Hence the claim is established. I now show that
$[\alpha]\,{\boldsymbol{\mathit{while}}}\ (B)\ P\
{\boldsymbol{\mathit{elihw}}}\,[\beta]$ holds. Assume execution starts in an
arbitrary $s\in\mathit{post}(\alpha)$ and that the loop terminates in some
state $t$. By the above claim, $t\in\mathit{post}(\alpha)$. Also,
$t(B)=\mathit{ff}$ since otherwise the loop cannot terminate in state $t$.
Hence $t\in\mathit{post}(\beta)$, and so
$[\alpha]\,{\boldsymbol{\mathit{while}}}\ (B)\ P\
{\boldsymbol{\mathit{elihw}}}\,[\beta]$ is established. Hence (While) is
sound. $\Box$

#### While Rule with Consequence.

By applying Proposition 1 and (Post-program Weakening) to (While), I obtain
(While Consequence), which states that the operational invariant can be a
“suffix” of the actual post-program of the loop body. This is often
convenient, in practice.

###### Theorem 10

(While Consequence) is sound, i.e., if the hypothesis is true, then so is the
conclusion.

Proof. Assume the hypothesis $[\alpha^{\prime}]\,P\,[\gamma;\alpha]$. By
Proposition 1, $\gamma;\alpha\preceq\alpha$. Hence by (Post-program
Weakening), $[\alpha^{\prime}]\,P\,[\alpha]$. Hence by (While),
$[\alpha]\,{\boldsymbol{\mathit{while}}}\ (B)\
P{\boldsymbol{\mathit{elihw}}}\,[\beta]$. $\Box$

#### If Rule.

Let $\alpha$ be the pre-program. Assume that execution of $P1$ with pre-
program $\alpha^{\prime}\cong(\alpha,B)$ leads to post-program $\beta$, and
that execution of $P2$ with pre-program
$\alpha^{\prime\prime}\cong(\alpha,\neg B)$ also leads to post-program
$\beta$. Then, execution of ${\boldsymbol{\mathit{if}}}\ {B}\
{\boldsymbol{\mathit{then}}}\ P1\ {\boldsymbol{\mathit{else}}}\ P2\
{\boldsymbol{\mathit{fi}}}$ with pre-program $\alpha$ leads to post-program
$\beta$.

###### Theorem 11

(If) is sound, i.e., if both hypotheses are true, then so is the conclusion.

Proof. Assume execution starts in an arbitrary $s\in\mathit{post}(\alpha)$.
Suppose that $B$ holds in $s$. Then, $s\in\mathit{post}(\alpha^{\prime})$.
Also, the ${\boldsymbol{\mathit{if}}}$ branch will be taken, so that $P1$ is
executed. Let $t$ be any resulting state. From the hypothesis
$[\alpha^{\prime}]\,P1\,[\beta]$, I have $t\in\mathit{post}(\beta)$. Now
suppose that $B$ does not hold in $s$. Then
$s\in\mathit{post}(\alpha^{\prime\prime})$. Also, the
${\boldsymbol{\mathit{else}}}$ branch will be taken, so that $P2$ is executed.
Let $t$ be any resulting state. From the hypothesis
$[\alpha^{\prime\prime}]\,P2\,[\beta]$, I have $t\in\mathit{post}(\beta)$. By
Definition 2, $[\alpha]\,{\boldsymbol{\mathit{if}}}\ {B}\
{\boldsymbol{\mathit{then}}}\ P1\ {\boldsymbol{\mathit{else}}}\ P2\
{\boldsymbol{\mathit{fi}}}\,[\beta]$ is valid. $\Box$

#### One-way If Rule.

Assume that execution of $P$ with pre-program $\alpha^{\prime}\cong(\alpha,B)$
leads to post-program $\beta$. Assume that any post-state of
$\alpha^{\prime\prime}\cong(\alpha,\neg B)$ is also a post-state of $\beta$.
Then execution of ${\boldsymbol{\mathit{if}}}\ {B}\
{\boldsymbol{\mathit{then}}}\ P\ {\boldsymbol{\mathit{fi}}}$ with pre-program
$\alpha$ always leads to post-program $\beta$.

###### Theorem 12

(One-way If) is sound, i.e., if both hypotheses are true, then so is the
conclusion.

Proof. Assume execution starts in an arbitrary $s\in\mathit{post}(\alpha)$.
Suppose that $B$ holds in $s$. Then, $s\in\mathit{post}(\alpha^{\prime})$.
Also, the ${\boldsymbol{\mathit{if}}}$ branch will be taken, so that $P$ is
executed. Let $t$ be any resulting state. From the hypothesis
$[\alpha^{\prime}]\,P\,[\beta]$, I have $t\in\mathit{post}(\beta)$. Now
suppose that $B$ does not hold in $s$. Then
$s\in\mathit{post}(\alpha^{\prime\prime})$. Now
$\alpha^{\prime\prime}\preceq\beta$, and so $s\in\mathit{post}(\beta)$ by Def.
3. Since the ${\boldsymbol{\mathit{if}}}$ branch is not taken, there is no
change of state, and so the resulting state $t$ is the same as $s$. Hence
$t\in\mathit{post}(\beta)$. By Definition 2,
$[\alpha]\,{\boldsymbol{\mathit{if}}}\ {B}\ {\boldsymbol{\mathit{then}}}\ P\
{\boldsymbol{\mathit{fi}}}\,[\beta]$. $\Box$

##  5 Examples

I now illustrate program verification with operational triples by means of
several examples. Throughout, I use an informally justified notion of program
equivalence, based on well-known transformations such as eliminating the empty
program $\mathit{skip}$, and unwinding the last iteration of a
${\boldsymbol{\mathit{for}}}$ loop. Specifications programs are written in
bold red italics, and regular programs are written in typewriter.

###  5.1 Example: selection sort

The input is an array $a$ and its size $n$, with $a$ indexed from 0 to $n-1$.
The assignment $i\colonequals[a:b]$ (with $a\leqslant b$) nondeterministically
chooses a value between $a$ and $b$ inclusive, and assigns it to $i$. The
following holds by (Empty Program). I will develop this into the loop body for
selection sort, which will be iterated for $i$ from 0 to $n-2$.
$\mathit{findRank}(a,I)$ returns the index of the rank $I$ element in array
$a$. In case of duplicates, I take the element with lower index to also be of
lower rank. This breaks ties for duplicates, and also ensures that the
resulting sort is stable. We can specify a non-stable sort by assigning the
rank randomly amongst duplicate values (within the appropriate range).

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{skip}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

Now unwind the last iteration of the loop in the pre-program:

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{J\colonequals\mathit{findRank}(a,i);a[i]\leftrightarrow
a[J]}}}$
$\mathit{\mathtt{\mathtt{skip}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

Now use (Trading) to move the third line of the pre-program into the program.
Then remove the $skip$, as it is no longer needed.

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{J\colonequals\mathit{findRank}(a,i);a[i]\leftrightarrow
a[J]}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

Now I compute $\mathit{findRank}(a,i)$ explicitly using an inner loop.
$\mathit{findMin}(a,\varphi)$ computes the location of the lowest minimum
element in array $a$, excluding the consideration of elements whose indices
are in the set $\varphi$.

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\varphi\colonequals\emptyset;{\boldsymbol{\mathit{for}}}\
(k=0\ {\boldsymbol{\mathit{to}}}\ i-1)\
\varphi\colonequals\varphi\cup\mathit{findMin}(a,\varphi){\boldsymbol{\mathit{rof}}}}}$
$\mathit{\mathtt{J\colonequals\mathit{findMin}(a,\varphi)}}$
$\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

Now use (Trading) to trade into the pre-program:

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{\varphi\colonequals\emptyset;{\boldsymbol{\mathit{for}}}\
(k=0\ {\boldsymbol{\mathit{to}}}\ i-1)\
\varphi\colonequals\varphi\cup\mathit{findMin}(a,\varphi){\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{J\colonequals\mathit{findMin}(a,\varphi)}}$
$\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

Now construct a sequence of equivalences on the pre-program

$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{\varphi\colonequals\emptyset;{\boldsymbol{\mathit{for}}}\
(k=0\ {\boldsymbol{\mathit{to}}}\ i-1)\
\varphi\colonequals\varphi\cup\mathit{findMin}(a,\varphi){\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\equiv}$
$\mathit{{\color[rgb]{1,0,0}\mathit{\varphi\colonequals\emptyset;}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J];\varphi\colonequals\varphi\cup\mathit{findMin}(a,\varphi){\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\equiv}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J];\varphi\colonequals\varphi\cup I{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\equiv}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{\varphi\colonequals\\{0,\ldots,i-1\\};}}}$

I therefore have, using (Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{\varphi\colonequals\\{0,\ldots,i-1\\};}}}$
$\mathit{\mathtt{J\colonequals\mathit{findMin}(a,\varphi)}}$
$\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

Now use (Trading) to trade into the program

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}}$
$\mathit{\mathtt{\varphi\colonequals\\{0,\ldots,i-1\\};}}$
$\mathit{\mathtt{J\colonequals\mathit{findMin}(a,\varphi)}}$
$\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

I now replace
$\varphi\colonequals\\{0,\ldots,i-1\\};J\colonequals\mathit{findMin}(a,\varphi)$
by the equivalent $J\colonequals\mathit{findMin}(a,[0:i-1])$, so that
$\mathit{findMin}(a,[0:i-1])$ finds a minimum element in array $a$ in the
range $i$ to $n-1$, since the indices in $[0:i-1]$ are excluded. Hence, by
(Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}}$
$\mathit{\mathtt{J\colonequals\mathit{findMin}(a,[0:i-1]);}}$
$\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

I now add the increment of $i$ at the end of the loop:

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}}$
$\mathit{\mathtt{J\colonequals\mathit{findMin}(a,[0:i-1]);}}$
$\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{i\colonequals i+1}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[1:n-1];}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}$

which gives the body of selection sort. I finish up the example by including
the outer loop

$\mathit{{\color[rgb]{1,0,0}\mathit{\mathit{skip}}}}$
---
$\mathit{\mathtt{i\colonequals 0}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals 0}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{{while}}\ (i\neq n-1)\ }}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{\mathtt{J\colonequals\mathit{findMin}(a,[0:i-1]);}}$
| $\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{\mathtt{i\colonequals i+1}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[1:n-1];}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}}$
$\mathit{\mathtt{\mathtt{{elihw}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals n-1}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

By applying (Post-program Weakening), I obtain

$\mathit{{\color[rgb]{1,0,0}\mathit{\mathit{skip}}}}$
---
$\mathit{\mathtt{i\colonequals 0}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals 0}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{{while}}\ (i\neq n-1)\ }}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{\mathtt{J\colonequals\mathit{findMin}(a,[0:i-1]);}}$
| $\mathit{\mathtt{a[i]\leftrightarrow a[J]}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:n-2];}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{\mathtt{i\colonequals i+1}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[1:n-1];}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ i-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}};}}}$
$\mathit{\mathtt{\mathtt{{elihw}}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (I=0\
{\boldsymbol{\mathit{to}}}\ n-1)\
J\colonequals\mathit{findRank}(a,I);a[I]\leftrightarrow
a[J]{\boldsymbol{\mathit{rof}}}}}$

The post-program states that the element at index $I$ has rank $I$, that is,
array $a$ is sorted. I omit the development of $\mathit{findMin}$.

###  5.2 Example: Dijkstra’s shortest paths algorithm

The input consists of the following:

  * •

a directed graph $G=(V,E)$ with node set $V$ and edge set $E$, together with a
weight function $w:E\to\mathit{\mathbf{R}}^{\geqslant 0}$, since Dijkstra’s
algorithm requires that edge weights are non-negative.

  * •

a distinguished vertex $s$: the source.

  * •

for each node $t$, a real number $t.d$, which records the current estimate of
the shortest path distance from the source $s$ to $t$

I use $\delta[t]$ to denote the shortest path distance from the source $s$ to
node $t$, and $u\rightarrow v$ to mean $(u,v)\in E$, i.e., there is an edge in
$G$ from $u$ to $v$.

Dijkstra’s algorithm is incremental, each iteration of the main loop computes
the shortest path distance of some node $m$. Vertices are colored black
(shortest path distance from the source $s$ is known), grey (have an incoming
edge form a black node), and white (neither black nor grey). The algorithm
maintains the sets $B$ and $G$ of black and grey nodes.

I start with an instance of (Empty Program). The assignment $B\colonequals?$
nondeterministically sets $B$ to any subset of $V$ which contains the source
$s$. It can be implemented using the nondeterministic choice operator []
(Section 2). The pre- and post-programs simply assign the correct shortest
path distances to the $t.d$ variable for each node $t$ in $B$.

$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{skip}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}$

Now append to both the pre- and post-programs a statement which relaxes all of
the grey nodes. This is still an instance of (Empty Program).

$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{skip}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}$

Apply (Append) to add “$m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)$;
$m.d\colonequals(\mathrm{MIN}\,\pi\in paths(s,m):|\pi|)$” to both program and
post-program, and also remove the $\mathtt{skip}$, as it is no longer needed.
$|\pi|$ is the total cost of path $\pi$, and $paths(s,m)$ is the set of all
simple paths from $s$ to $m$.

$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}$
$\mathit{\mathtt{m.d\colonequals(\mathrm{MIN}\,\pi\in paths(s,m):|\pi|)}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{m\colonequals\\{g\ |\
g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{m.d\colonequals(\mathrm{MIN}\,\pi\in
paths(s,m):|\pi|)}}}$

Now construct a sequence of equivalences as follows:

$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
---
$\equiv$ // definition of relax(b,g)
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\ g.d\colonequals
g.d\min b.d+w(b,g)){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\equiv$ // min is commutative and associative
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
g.d\colonequals g.d\min\ (\mathrm{MIN}\,b\in B\land b\rightarrow
g:b.d+w(b,g)){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\equiv$ // use the operational invariant
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
g.d\colonequals g.d\min\ (\mathrm{MIN}\,b\in B\land b\rightarrow
g:\delta[b]+w(b,g)){\boldsymbol{\mathit{rof}}}}}}$
$\equiv$ // $s\mbox{$\,\stackrel{{\scriptstyle B}}{{\rightarrow}}\,$}g$
denotes all paths from $s$ to $g$ containing only black nodes except $g$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
g.d\colonequals g.d\min\ (\mathrm{MIN}\,\pi\in
s\mbox{$\,\stackrel{{\scriptstyle
B}}{{\rightarrow}}\,$}g:|\pi|){\boldsymbol{\mathit{rof}}}}}}$
$\equiv$ // $s\mbox{$\,\stackrel{{\scriptstyle}}{{\rightarrow}}\,$}g$ denotes
all paths from $s$ to $g$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
g.d\colonequals g.d\min\ (\mathrm{MIN}\,\pi\in
s\mbox{$\,\stackrel{{\scriptstyle
B}}{{\rightarrow}}\,$}g:|\pi|){\boldsymbol{\mathit{rof}}};}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in M)\
g.d\colonequals g.d\min\ (\mathrm{MIN}\,\pi\in
s\mbox{$\,\stackrel{{\scriptstyle B}}{{\rightarrow}}\,$}g:|\pi|)\min\
(\mathrm{MIN}\,\pi\in
s\mbox{$\,\stackrel{{\scriptstyle}}{{\rightarrow}}\,$}g:|\pi|){\boldsymbol{\mathit{rof}}}}}}$
$\equiv$ // definition of $\delta$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
g.d\colonequals g.d\min\ (\mathrm{MIN}\,\pi\in
s\mbox{$\,\stackrel{{\scriptstyle
B}}{{\rightarrow}}\,$}g:|\pi|){\boldsymbol{\mathit{rof}}};}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in M)\
g.d\colonequals\delta[g]}}}$

The above equivalence allows me to conclude the following:

$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}$
$\mathtt{m.d\colonequals(\mathrm{MIN}\,\pi\in paths(s,m):|\pi|)}$

is equivalent to

$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathtt{m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}$

I also observe that
${\color[rgb]{1,0,0}\mathit{m.d\colonequals(\mathrm{MIN}\,\pi\in
paths(s,m):|\pi|)}}$ is equivalent to
${\color[rgb]{1,0,0}\mathit{m.d\colonequals\delta[m]}}$ by definition of
$\delta[m]$, the shortest path distance from source $s$ to node $m$. Hence, by
(Substitution) I can now write

$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{m\colonequals\\{g\ |\
g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}}$
${\color[rgb]{1,0,0}\mathit{m.d\colonequals\delta[m]}}$

Now color $m$ black. This causes, in general, some nodes to turn grey, and so
requires the addition of the line $\mathtt{{\boldsymbol{\mathit{for}}}\ (g\in
G\land m\rightarrow g)\ relax(m,g)}$ to preserve the truth of the operational
triple. I retain the intermediate specification program between the program
statement that selects $m$, and the statements which turn $m$ black and then
relax all of $m$’s grey neighbors. The assignment $B\colonequals?^{\prime}$
nondeterministically sets $B$ to any subset of $V$ which contains both $s$ and
$m$.

$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{m\colonequals\\{g\ |\
g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{m.d\colonequals\delta[m]}}}$
$\mathit{\mathtt{B\colonequals B\cup\left\\{m\right\\};}}$
$\mathit{\mathtt{\mathtt{{for}}\ (g\in G\land m\rightarrow g)\ relax(m,g)}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?^{\prime}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}$

This concludes the development of the loop body. The pre-program consists of
making the looping condition true followed by the specification program

$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}$

and the post-program has this specification program as a suffix. Hence this
specification program plays the role of an “invariant”, and we have, by (While
Consequence), the complete annotated program:

$\mathit{{\color[rgb]{1,0,0}\mathit{skip}}}$
---
$\mathit{\mathtt{B\colonequals\left\\{s\right\\};s.d\colonequals
0;{\boldsymbol{\mathit{for}}}\ (t\not\in B)\
t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{{while}}\ (B\neq V)\ }}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{\mathtt{m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{m\colonequals\\{g\ |\
g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{m.d\colonequals\delta[m]}}}$
| $\mathit{\mathtt{B\colonequals B\cup\left\\{m\right\\}}}$
| $\mathit{\mathtt{\mathtt{{for}}\ (g\in G\land m\rightarrow g)\ relax(m,g)}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?^{\prime}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{{elihw}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals V}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}$

By applying (Post-program Weakening), I obtain

$\mathit{{\color[rgb]{1,0,0}\mathit{skip}}}$
---
$\mathit{\mathtt{B\colonequals\left\\{s\right\\};s.d\colonequals
0;{\boldsymbol{\mathit{for}}}\ (t\not\in B)\
t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{{while}}\ (B\neq V)\ }}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{\mathtt{m\colonequals\\{g\ |\ g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{m\colonequals\\{g\ |\
g.d=(\mathrm{MIN}\,h\in G:h.d)\\}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{m.d\colonequals\delta[m]}}}$
| $\mathit{\mathtt{B\colonequals B\cup\left\\{m\right\\}}}$
| $\mathit{\mathtt{\mathtt{{for}}\ (g\in G\land m\rightarrow g)\ relax(m,g)}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{B\colonequals?^{\prime}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in B)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}};{\boldsymbol{\mathit{for}}}\
(t\not\in B)\ t.d\colonequals+\infty{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (g\in G)\
{\boldsymbol{\mathit{for}}}\ (b\in B\land b\rightarrow g)\
relax(b,g){\boldsymbol{\mathit{rof}}}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{\mathtt{{elihw}}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (t\in V)\
t.d\colonequals\delta[t]{\boldsymbol{\mathit{rof}}}}}$

The post-program sets the $t.d$ variable for every node $t$ to the correct
shortest path value.

###  5.3 Example: in-place list reversal

I now illustrate the use of operational annotations to derive a correct
algorithm for the in-place reversal of a linked list. The input is a size
$\ell>0$ array $n$ of objects of type $Node$, indexed from 0 to $\ell-1$.
$Node$ is declared as follows: ${\color[rgb]{1,0,0}\mathit{class\ Node\\{Node\
p;\ \mbox{other fields}\ldots\\}}}$. Element $i$ is referred to as $n_{i}$
instead of $n[i]$, and contains a pointer $n_{i}.p$, and possibly other
(omitted) fields. The use of this array is purely for specification purposes,
so that I can go through the nodes and construct the linked list, which is
then reversed. An array also ensures that there is no aliasing: all elements
are distinct, by construction. Array $n$ is created by executing
${\color[rgb]{1,0,0}\mathit{Node[\,]\ n\colonequals new\ Node[\ell]}}$. The
pre-program and post-program both start with code to declare $Node$, followed
by the above line to create array $n$. I omit this code as including it would
be repetitive and would add clutter.

I start by applying (Empty Program). The pre (and post) programs do 3 things:
(1) construct the linked list, (2) reverse part of the list, up to position
$i+1$, and (3) maintain 3 pointers, into positions $i+1$, $i+2$, and $i+3$.

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}}$
$\mathit{\mathtt{\mathtt{skip}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

Now unwind the last iteration of the second ${\boldsymbol{\mathit{for}}}$ loop
of the pre-program. So, by (Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{n_{i+1}.p\colonequals n_{i};}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}}$
$\mathit{\mathtt{\mathtt{skip}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

Now introduce the line $r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}$ into the pre-program. Since $r,s,t$ are
subsequently overwritten, and not referenced in the interim, this preserves
equivalence of the pro-program with its previous version. So, by
(Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{n_{i+1}.p\colonequals n_{i};}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}}$
$\mathit{\mathtt{\mathtt{skip}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

Now apply (Trading) to trade into the program, and remove the $\mathit{skip}$
since it is no longer needed.

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{n_{i+1}.p\colonequals n_{i};}}$
$\mathit{\mathtt{r\colonequals n_{i+1};s\colonequals n_{i+2};t\colonequals
n_{i+3}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

Since ${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals n_{i+1}}}$
immediately precedes $\mathtt{n_{i+1}.p\colonequals n_{i}}$, I can replace
$\mathtt{n_{i+1}.p\colonequals n_{i}}$ by $\mathtt{s.p\colonequals r}$ while
retaining equivalence. So, by (Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{s.p\colonequals r;}}$
$\mathit{\mathtt{r\colonequals n_{i+1};s\colonequals n_{i+2};t\colonequals
n_{i+3}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

Since ${\color[rgb]{1,0,0}\mathit{s\colonequals n_{i+1}}}$ precedes
$\mathtt{r\colonequals n_{i+1}}$ and $s$ is not modified in the interim, I can
replace $\mathtt{r\colonequals n_{i+1}}$ by $\mathtt{r\colonequals s}$ while
retaining equivalence. So, by (Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{s.p\colonequals r;}}$
$\mathit{\mathtt{r\colonequals s;s\colonequals n_{i+2};t\colonequals
n_{i+3}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

In a similar manner, I can replace $\mathtt{s\colonequals n_{i+2}}$ by
$\mathtt{s\colonequals t}$. So, by (Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{i+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{s.p\colonequals r;}}$
$\mathit{\mathtt{r\colonequals s;s\colonequals t;t\colonequals n_{i+3}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{i+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

From ${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{i+1}{\boldsymbol{\mathit{rof}}}}}$, I have
${\color[rgb]{1,0,0}\mathit{n_{i+2}.p\colonequals n_{i+3}}}$, and I observe
that $n_{i+2}.p$ is not subsequently modified. Also I have
${\color[rgb]{1,0,0}\mathit{t\colonequals n_{i+2}}}$ occurring before the
program, and $t$ is not modified until $\mathtt{t\colonequals n_{i+3}}$, we
can replace $\mathtt{t\colonequals n_{i+3}}$ by $\mathtt{t\colonequals t.p}$.
So, by (Substitution)

$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
---
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{s.p\colonequals r;}}$
$\mathit{\mathtt{r\colonequals s;s\colonequals t;t\colonequals t.p}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}$

Now apply (While) to obtain the complete program, while also incrementing the
loop counter $i$ at the end of the loop body.

$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
---
$\mathit{\mathtt{r\colonequals n_{0};s\colonequals n_{1};t\colonequals
n_{2}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals 0}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{i+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{\mathtt{{while}}\ (i\neq\ell-2)\ }}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
| $\mathit{\mathtt{s.p\colonequals r;}}$
| $\mathit{\mathtt{r\colonequals s;s\colonequals t;t\colonequals t.p}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}}$
| $\mathit{\mathtt{i\colonequals i+1;}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[1:\ell-2]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{\mathtt{{elihw}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals\ell-2}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}$

The loop must terminate at $i=\ell-2$ to avoid dereferencing nil. The post-
program of the loop then gives
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=\ell-2\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}$, which means that the last node’s
pointer is not set to the previous node, since the list ends at index
$\ell-1$. Hence we require a final assignment that is equivalent to
$n_{\ell-1}.p\colonequals n_{\ell-2}$.

The post-program of the loop gives
${\color[rgb]{1,0,0}\mathit{i\colonequals\ell-2;r\colonequals
n_{i};s\colonequals n_{i+1};t\colonequals n_{i+2}}}$, which yields
${\color[rgb]{1,0,0}\mathit{i\colonequals\ell-2;r\colonequals
n_{\ell-2};s\colonequals n_{\ell-1};t\colonequals n_{\ell}}}$. Hence the last
assignment can be rendered as $s.p\colonequals r$. Also, the loop termination
condition can be rewritten as $t\neq\mbox{{nil}}$, since $t$ becomes nil when
it is assigned $n_{\ell}$, which happens exactly when $i$ becomes $\ell-2$.
Hence, using (Substitution) and (Post-program Weakening), I obtain

$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
---
$\mathit{\mathtt{r\colonequals n_{0};s\colonequals n_{1};t\colonequals
n_{2}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals 0}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{i+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{\mathtt{{while}}\ (t\neq\mbox{{nil}})\ }}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
| $\mathit{\mathtt{s.p\colonequals r;}}$
| $\mathit{\mathtt{r\colonequals s;s\colonequals t;t\colonequals t.p}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i+1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i+1};s\colonequals
n_{i+2};t\colonequals n_{i+3}}}}$
| $\mathit{\mathtt{i\colonequals i+1;}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[1:\ell-2]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{\mathtt{{elihw}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals\ell-2}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{s.p\colonequals r;}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=\ell-1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$

Now, as desired, the “loop counter” $i$ is no longer needed as a program
variable, and can be converted to an auxiliary (“ghost”) variable. The result
is

$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
---
$\mathit{\mathtt{r\colonequals n_{0};s\colonequals n_{1};t\colonequals
n_{2}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals 0}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{i+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{\mathtt{{while}}\ (t\neq\mbox{{nil}})\ }}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[0:\ell-3]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
| $\mathit{\mathtt{s.p\colonequals r;}}$
| $\mathit{\mathtt{r\colonequals s;s\colonequals t;t\colonequals t.p}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals[1:\ell-2]}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
| $\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{\mathtt{\mathtt{{elihw}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{i\colonequals\ell-2}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{r\colonequals n_{i};s\colonequals
n_{i+1};t\colonequals n_{i+2}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=i\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{\mathtt{s.p\colonequals r;}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=0\
{\boldsymbol{\mathit{to}}}\ \ell-1)\ n_{j}.p\colonequals
n_{j+1}{\boldsymbol{\mathit{rof}}}}}}$
$\mathit{{\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{for}}}\ (j=\ell-1\
{\boldsymbol{\mathit{downto\ }}}1)\ n_{j}.p\colonequals
n_{j-1};{\boldsymbol{\mathit{rof}}}}}}$

Upon termination, $\mathtt{s}$ points to the head of the reversed list. The
post-program is quite pleasing: it constructs the list, and then immediately
reverses it!

##  6 Operational annotations with non-recursive procedures

Let $pname$ be a non-recursive procedure with parameter passing by value, and
with body $pbody$. Let $\overline{a}$ denote a list of actual parameters, and
let $\overline{f}$ denote a list of formal parameters. An actual parameter is
either an object identifier or an expression over primitive types, and a
formal parameter is either an object identifier or a primitive-type
identifier. I handle non-recursive procedures in a similar manner to Hoare
logic verification rules for non-recursive procedures [6]: formal parameters
are replaced by actual parameters. The most convenient expression of this
principle is as an equivalence between a procedure call and an instance of the
procedure body with the appropriate assignment of actuals to formals. The
equivalence rules for non-recursive procedure calls are:

$pname(\overline{a})\;\equiv\;\overline{f}\colonequals\overline{a};pbody$
(Equiv Nonrecursive Void) $r\colonequals
pname(\overline{a})\;\equiv\;\overline{f}\colonequals\overline{a};pbody[r\colonequals
e/{\boldsymbol{\mathit{return}}}(e)]$ (Equiv Nonrecursive)

Rule Equiv Nonrecursive is for when no value is returned (procedure type is
void), or the returned value is not saved by being assigned to a variable
(return value is “thrown away”). In this case, the form of the procedure call
is $pname(\overline{a})$, i.e., the procedure name followed by the actual
parameter list. Rule Equiv Nonrecursive then assigns the formals to the
actuals (I assume a multiple assignment, with the obvious semantics) and
executes the procedure body.

Rule Equiv Nonrecursive is for when the returned value is assigned to a
variable. In this case, the form of the procedure call is $r\colonequals
pname(\overline{a})$, i.e., an assignment statement in which the value
returned by the call $pname(\overline{a})$ is saved in variable $r$. Rule
Equiv Nonrecursive then assigns the formals to the actuals (I assume a
multiple assignment, with the obvious semantics) and executes a modified
procedure body in which

I now give two examples of application of the above rules: selection sort and
linked list reversal. First, consider the selection sort algorithm developed
above, packaged as a procedure:

$\mathit{\mathtt{void\ Procedure\ sort(int[]\ a,\ int\ n)\\{}}$
---
| $\mathit{\mathtt{i\colonequals 0}}$
| $\mathit{\mathtt{\mathtt{{while}}\ (i\neq n-1)\ }}$
|  | $\mathtt{J\colonequals\mathit{findMin}(i:n-1);}$
|  | $\mathtt{a[i]\leftrightarrow a[J]}$
|  | $\mathtt{i\colonequals i+1}$
| $\mathit{\mathtt{\mathtt{{elihw}}}}$
$\\}$

Now consider a call $sort(b,m)$ where $b$ is an array of length $m$. By (Equiv
Nonrecursive Void), I have

$\mathit{\mathtt{sort(b,m)\;\equiv\;\\{}}$
---
| $\mathit{a:=b;n:=m;}$
| $\mathit{\mathtt{i\colonequals 0}}$
| $\mathit{\mathtt{\mathtt{{while}}\ (i\neq n-1)\ }}$
|  | $\mathtt{J\colonequals\mathit{findMin}(a,[0:i-1]);}$
|  | $\mathtt{a[i]\leftrightarrow a[J]}$
|  | $\mathtt{i\colonequals i+1}$
| $\mathit{\mathtt{\mathtt{{elihw}}}}$
|  $\mathtt{\\}}$

This clearly has the correct effect. Now, consider the linked list reversal
algorithm above, also packaged as a procedure:

$\mathit{\mathtt{Node\ Procedure\ listRev(Node\ h)}\ \\{}$
---
| $\mathit{\mathtt{r\colonequals h;s\colonequals h.next;t\colonequals
h.next.next;}}$
| $\mathit{\mathtt{\mathtt{{while}}\ (t\neq\mbox{{nil}})\ }}$
|  | $\mathtt{s.p\colonequals r;}$
|  | $\mathtt{r\colonequals s;s\colonequals t;t\colonequals t.p}$
| $\mathit{\mathtt{\mathtt{{elihw}};}}$
| $\mathit{\mathtt{s.p\colonequals r;}}$
| $\mathit{\mathtt{\mathtt{{return}}(s)}}$
$\mathtt{\\}}$

Now consider a call $v\colonequals listRev(\ell)$ where $\ell$ is the head of
a linked list. By (Equiv Nonrecursive), I have:

$\mathit{\mathtt{v\colonequals listRev(\ell)\;\equiv\\{}}$
---
| $\mathit{\mathtt{h\colonequals\ell;}}$
| $\mathit{\mathtt{r\colonequals h;s\colonequals h.next;t\colonequals
h.next.next;}}$
| $\mathit{\mathtt{\mathtt{{while}}\ (t\neq\mbox{{nil}})\ }}$
|  | $\mathtt{s.p\colonequals r;}$
|  | $\mathtt{r\colonequals s;s\colonequals t;t\colonequals t.p}$
| $\mathit{\mathtt{\mathtt{{elihw}};}}$
| $\mathit{\mathtt{s.p\colonequals r;}}$
| $\mathit{\mathtt{v\colonequals s}}$
|  $\\}$

Again, this gives the correct effect for the procedure call $listRev(\ell)$,
namely that $v$ points to the head of the reversed list. Note that both
primitive and reference types (as parameters) are handled correctly, and need
not be distinguished in the above rules.

##  7 Operational annotations with recursive procedures

For recursive procedures, it is not sufficient to simply replace the call by
the body, since the body contains recursive instances of the call. Clearly an
inductive proof method is needed. What I use is an inductive rule to establish
the equivalence between a sequence of two procedure calls and a third
procedure call. These correspond, respectively, to the pre-program, the
program, and the post-program. The method is as follows:

  1. 1.

Let $\alpha,P,\beta$ be recursive procedures which give, respectively, the
pre-program, program, and post-program

  2. 2.

To establish $\alpha;P\equiv\beta$ I proceed as follows:

    1. (a)

Start with $\alpha;P$, replace the calls by their corresponding bodies, and
then use sequence of equivalence-preserving transformations to bring the
recursive calls of $\alpha^{\prime};P^{\prime}$ next to each other

    2. (b)

Use the inductive hypothesis for equivalence of the recursive calls
$\alpha^{\prime};P^{\prime}\equiv\beta^{\prime}$ to replace
$\alpha^{\prime};P^{\prime}$ by $\beta^{\prime}$

    3. (c)

Use more equivalence-preserving transformations to show that the resulting
program is equivalent to $\beta$

The appropriate rule of inference is as follows:

$\frac{\begin{array}[]{l}\alpha^{\prime};P^{\prime}\equiv\beta^{\prime}\
\vdash\ \alpha;P\equiv\beta\end{array}}{\alpha;P\equiv\beta}$ (Equiv
Recursive)

where $\vdash$ means “is deducible from”, as usual. This states that if we can
prove $\alpha;P\equiv\beta$ (pre-program followed by program is equivalent to
post-program) by assuming $\alpha^{\prime};P^{\prime}\equiv\beta^{\prime}$ (a
recursive invocation of the pre-program followed by a recursive invocation of
the program is equivalent to a recursive invocation of the post-program), then
we can conclude, by induction on recursive calls, that $\alpha;P\equiv\beta$.

I illustrate this approach with an example which verifies the standard
recursive algorithm for inserting a node into a binary search tree (BST). Each
node $n$ in the tree consists of three fields: $n.\mathit{key}$ gives the key
value for node $n$, $n.\ell$ points to the left child of $n$ (if any), and
$n.r$ points to the right child of $N$ (if any). The constructor
${\boldsymbol{\mathit{Node}}}(v)$ returns a new node with key value $v$ and
null left and right child pointers. I assume that all key values in the tree
are unique.

The procedure $\mathit{insert}{(t,v)}$ gives the standard recursive algorithm
for insertion of key $v$ into a BST with root $t$.

$\mathtt{\underline{\mathit{insert}{(T,k)}}}$::
---
$\mathtt{\mathtt{{if}}\ (T=\mbox{{nil}})T\colonequals{\mathtt{{new}}\
{\boldsymbol{\mathit{Node}}}(k)};}$
$\mathtt{\mathtt{{else\ if}}\ (k<T.\mathit{key})\
\mathit{insert}{(T.\ell,k)};}$
$\mathtt{\mathtt{{else}}\ \mathit{insert}{(T.r,k)}}$;
//$\mathtt{k>T.\mathit{key}}$

To verify the correctness of $\mathit{insert}{(T,k)}$, I define two recursive
procedures as follows.

The recursive procedure $\mathit{ct}{(T,\psi)}$ takes a set $\psi$ of key
values, and constructs a random binary search tree which contains exactly
these values, and sets $T$ to point to the root of this tree. The statement
$x\colonequals select\ in\ \psi$ selects a random value in $\psi$ and assigns
it to $x$.

The recursive procedure $\mathit{cti}{(T,\psi,k)}$ takes a set $\psi$ of key
values and a key value $k\not\in\psi$, constructs a random binary search tree
which contains exactly the values in $\psi$ together with the key $k$, and
where $k$ is a leaf node, and sets $T$ to point to the root of this tree.

|  ${\color[rgb]{1,0,0}\mathit{\underline{\mathit{ct}{(T,\psi)}}}}$::
---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\ (\psi=\emptyset)\
T\colonequals\mbox{{nil}};}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \psi;}}$
${\color[rgb]{1,0,0}\mathit{\psi\colonequals\psi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\psi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\psi\land
y>x\right\\})};}}$

|  |  ${\color[rgb]{1,0,0}\mathit{\underline{\mathit{cti}{(T,\psi,k)}}}}$::
---|---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\ (\psi=\emptyset)\
T\colonequals{{\boldsymbol{\mathit{new}}}\
{\boldsymbol{\mathit{Node}}}(k)}}}$;
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \psi;}}$
${\color[rgb]{1,0,0}\mathit{\psi\colonequals\psi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
n\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\ (k<x)\ }}$
| ${\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T.\ell,\left\\{y\ |\ y\in\psi\land
y<x\right\\},k)};}}$
| ${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\psi\land
y>x\right\\})}}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
| ${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\psi\land
y<x\right\\})}}}$
|  ${\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T.r,\left\\{y\ |\ y\in\psi\land
y>x\right\\},k)};}}$ //$k>x$

I now verify

$[{\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}}]\,\mathtt{\mathit{insert}{(T,k)}}\,[{\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi\cup
k)}}}].$

That is, the pre-program creates a random BST with key values in $\varphi$ and
sets $T$ to the root, and the post-program creates a random BST with key
values in $\varphi\cup k$ and sets $T$ to the root. Hence, the above
operational triple states that the result of
$T\colonequals\mathit{insert}{(T,k)}$ is to insert key value $k$ into the BST
rooted at $T$. I first establish

$\mathit{cti}{(T,\varphi,k)}\preceq\mathit{ct}{(T,\varphi\cup k)}.$

Intuitively, this follows since $\mathit{cti}{(T,\varphi,k)}$ constructs a BST
with key values in $\varphi\cup k$, and where $k$ is constrained to be a leaf
node, while $\mathit{ct}{(T,\varphi\cup k)}$ constructs a BST with key values
in $\varphi\cup k$, with no constraint of where $k$ can occur. A formal proof
proceeds by induction on the length of an arbitrary execution $\pi$ of
$\mathit{cti}{(T,\varphi,k)}$, which shows that $\pi$ is also a possible
execution of $\mathit{ct}{(T,\varphi\cup k)}$. Recall that the use of the
random selection statement means that there are, in general, many possible
executions for a given input. The details are straightforward and are omitted.

In the sequel, I show that

$[{\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}}]\,\mathtt{\mathit{insert}{(T,k)}}\,[{\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T,\varphi,k)}}}]$

is valid. From (a,b) and (Post-program Weakening), I conclude that

$[{\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}}]\,\mathtt{\mathit{insert}{(T,k)}}\,[{\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi\cup
k)}}}]$

is valid, as desired. To establish (b), I show

${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}};\mathtt{\mathit{insert}{(T,k)}}\equiv{\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T,\varphi,k)}}}.$

from which (b) follows immediately by Definitions 4 and 2.

I establish (c) by using induction on recursive calls. I replace the above
calls by the corresponding procedure bodies, and then assume as inductive
hypothesis (c) as applied to the recursive calls within the bodies. This is
similar to the Hoare logic inference rule for partial correctness of recursive
procedures [6].

To be able to apply the inductive hypothesis, I take the sequential
composition
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}};\mathtt{\mathit{insert}{(T,k)}}$,
replace each call by the corresponding procedure body, and then I “interleave”
the procedure bodies using commutativity of statements. This enables me to
bring the recursive calls to $ctr$ and to $tinsrt$ together, so that the
inductive hypothesis can apply to their sequential composition, which can then
be replaced by the equivalent recursive call to $cti$. This results in
procedure body that corresponds to a call of $cti$, which completes the
equivalence proof. I first replace
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}}$ by the procedure body
that results from parameter binding:

| ${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\ (\varphi=\emptyset)\
T\colonequals\mbox{{nil}};}}$
---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \varphi;}}$
${\color[rgb]{1,0,0}\mathit{\varphi\colonequals\varphi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$

I now take $\mathtt{\mathit{insert}{(T,k)}}$ and place it at the end of both
the if branch and the else branch, which clearly preserves equivalence with
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}};\mathtt{\mathit{insert}{(T,k)}}$:

|  ${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\
(\varphi=\emptyset)\ T\colonequals\mbox{{nil}};}}$
$\mathtt{\mathit{insert}{(T,k)}}$
---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \varphi;}}$
${\color[rgb]{1,0,0}\mathit{\varphi\colonequals\varphi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$
$\mathtt{\mathit{insert}{(T,k)}}$

I replace $\mathtt{\mathit{insert}{(T,k)}}$ by the procedure body that results
from parameter binding:

|  $\mathtt{\mathtt{{if}}\ (T=\mbox{{nil}})\ T\colonequals{\mathtt{{new}}\
{\boldsymbol{\mathit{Node}}}(k)}}$;
---|---
$\mathtt{\mathtt{{else\ if}}\ (k<T.val)\ \mathit{insert}{(T.\ell,k)}}$
$\mathtt{\mathtt{{else}}\ \mathit{insert}{(T.r,k)}}$ //$k>T.val$

In the if branch, I have
${\color[rgb]{1,0,0}\mathit{T\colonequals\mbox{{nil}}}}$, and so the body of
$\mathtt{\mathit{insert}{(T,k)}}$ simplifies to

$\mathtt{T\colonequals{\mathtt{{new}}\ {\boldsymbol{\mathit{Node}}}(k)}}$.

In the else branch, I have
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$,
and so the body of $\mathtt{\mathit{insert}{(T,k)}}$ simplifies to

| $\mathtt{\mathtt{{if}}\ (k<T.val)\ \mathit{insert}{(T.\ell,k)}}$
---|---
$\mathtt{\mathtt{{else}}\ \mathit{insert}{(T.r,k)}}$ //$k>T.val$

I therefore now have

|  ${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\
(\varphi=\emptyset)\ T\colonequals\mbox{{nil}};}}$
$\mathtt{T\colonequals{\mathtt{{new}}\ {\boldsymbol{\mathit{Node}}}(k)}}$
---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \varphi;}}$
${\color[rgb]{1,0,0}\mathit{\varphi\colonequals\varphi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$
$\mathtt{\mathtt{{if}}\ (k<T.val)\mathit{insert}{(T.\ell,k)}}$
$\mathtt{\mathtt{{else}}\ \mathit{insert}{(T.r,k)}}$ //$k>T.val$

It is immediate that
${T\colonequals\mbox{{nil}};}\mathtt{T\colonequals{\mathtt{{new}}\
{\boldsymbol{\mathit{Node}}}(k)}}\equiv\mathtt{T\colonequals{\mathtt{{new}}\
{\boldsymbol{\mathit{Node}}}(k)}}$. I also move

| ${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\
y\in\varphi\land y<x\right\\})};}}$
---|---
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$

down into both branches of the following ${\boldsymbol{\mathit{if}}}\ $
statement:

|  ${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\
(\varphi=\emptyset)\ }}$ $\mathtt{T\colonequals{\mathtt{{new}}\
{\boldsymbol{\mathit{Node}}}(k)}}$
---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \varphi;}}$
${\color[rgb]{1,0,0}\mathit{\varphi\colonequals\varphi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
$\mathtt{\mathtt{{if}}\ (k<T.val)}$
$\mathtt{\mathit{insert}{(T.\ell,k)}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$
$\mathtt{\mathtt{{else}}\ }$ //$k>T.val$
$\mathit{insert}{(T.r,k)}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$

Since $\mathit{insert}{(T.r,k)}$ and
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$ commute, the above is equivalent to

|  ${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\
(\varphi=\emptyset)\ }}$ $\mathtt{T\colonequals{\mathtt{{new}}\
{\boldsymbol{\mathit{Node}}}(k)}}$
---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \varphi;}}$
${\color[rgb]{1,0,0}\mathit{\varphi\colonequals\varphi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
$\mathtt{\mathtt{{if}}\ (k<T.val)}$
$\mathtt{\mathit{insert}{(T.\ell,k)}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$
$\mathtt{\mathtt{{else}}\ }$ //$k>T.val$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
$\mathit{insert}{(T.r,k;)}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})}}}$

I now apply the inductive hypothesis to conclude that

$\mathtt{\mathit{insert}{(T.\ell,k)}}$;
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$ $\equiv$
${\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T.\ell,\left\\{y\ |\
y\in\varphi\land y<x\right\\},k)};}}$

and that

$\mathit{insert}{(T.r,k)}$;
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})}}}$ $\equiv$
${\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\},k)};}}$

Making these substitutions results in:

|  ${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{if}}}\
(\varphi=\emptyset)\ }}$ $\mathtt{T\colonequals{\mathtt{{new}}\
{\boldsymbol{\mathit{Node}}}(k)}}$
---|---
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{else}}}\ }}$
${\color[rgb]{1,0,0}\mathit{x\colonequals select\ in\ \varphi;}}$
${\color[rgb]{1,0,0}\mathit{\varphi\colonequals\varphi-x;}}$
${\color[rgb]{1,0,0}\mathit{{\boldsymbol{\mathit{Node}}}\
T\colonequals{\boldsymbol{\mathit{new}}}\ {\boldsymbol{\mathit{Node}}}(x);}}$
$\mathtt{\mathtt{{if}}\ (k<T.val)}$
${\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T.\ell,\left\\{y\ |\
y\in\varphi\land y<x\right\\},k)};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\})};}}$
$\mathtt{\mathtt{{else}}\ }$ //$k>T.val$
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T.\ell,\left\\{y\ |\ y\in\varphi\land
y<x\right\\})};}}$
${\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T.r,\left\\{y\ |\ y\in\varphi\land
y>x\right\\},k)};}}$

and the above is seen to be the procedure body corresponding to the call
${\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T,\varphi,k)}}}$.

The above was formed by starting with
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}};\mathtt{\mathit{insert}{(T,k)}}$,
replacing the calls by the procedure bodies, and then performing a sequence of
equivalence-preserving transformations. Hence I conclude
${\color[rgb]{1,0,0}\mathit{\mathit{ct}{(T,\varphi)}}};\mathtt{\mathit{insert}{(T,k)}}\equiv{\color[rgb]{1,0,0}\mathit{\mathit{cti}{(T,\varphi,k)}}}$,
which is (c) above. This completes the proof. For clarity, I have retained the
formatting of pre-/post-program code in red italics and of program code in
black typewriter, even as I was mixing these to establish the above
equivalence.

##  8 Related Work

The use of assertions to verify programs was introduced by Floyd [5] and Hoare
[9]: a precondition $f$ expresses what can be assumed to hold before execution
of a program $P$, and a postcondition $g$ expresses what must hold after the
statement. The “Hoare triple” $\\{f\\}\,P\,\\{g\\}$ thus states that if $f$
holds when execution of $P$ starts, then $g$ will hold upon termination of
$P$. If termination is not assumed, this is known as _partial correctness_ ,
and if termination is assumed we have _total correctness_. Both precondition
and postcondition are expressed as a formula of a suitable logic, e.g., first
order logic.

Subsequently, Dijkstra introduced the _weakest precondition predicate
transformer_ [4]: $wp(P,g)$ is the weakest predicate $f$ whose truth before
execution of $P$ guarantees $g$ afterwards, if $P$ terminates. He then used
weakest preconditions to define a method for formally deriving a program from
a specification, expressed as a precondition-postcondition pair. Later, Hoare
observed that the Hoare triple can be expressed operationally, when he wrote
“$\\{p\\}\,q\,\\{r\\}\triangleq p;q<r$” in [10], but he does not seem to have
developed this observation into a proof system.

The formalization of both specifications and program correctness has lead to a
rich and extensive literature on program verification and refinement. Hoare’s
original rules [9] were extended to deal with non-determinism, fair selection,
and procedures [6]. Separation logic [24] was introduced to deal with pointer-
based structures.

A large body of work deals with the notion of _program refinement_ [1, 19]:
start with an initial artifact, which serves as a specification, and gradually
refine it into an executable and efficient program. This proceeds
incrementally, in a sequence of refinement steps, each of which preserves a
“refinement ordering” relation $\sqsubseteq$, so that we have
$P_{0}\sqsubseteq\ldots\sqsubseteq P_{n}$, where $P_{0}$ is the initial
specification and $P_{n}$ is the final program. Morgan [19] starts with a pre-
condition/post-condition specification and refines it into an executable
program using rules that are similar in spirit to Dijkstra’s weakest
preconditions [4]. Back and Wright [1] use _contracts_ , which consist of
assertions (failure to hold causes a breach of the contract), assumptions
(failure to hold causes vacuous satisfaction of the contract), and executable
code. As such, contracts subsume both pre-condition/post-condition pairs and
executable programs, and so serve as an artifact for the seamless refinement
of a pre-condition/post-condition specification into a program.

A related development has been the application of monads to programming [17,
18]. A monad is an endofunctor $T$ over a category $C$ together with a unit
natural transformation from $1_{C}$ (the identity functor over $C$) to $T$ and
a multiplication natural transformation from $T^{2}$ to $T$. The Hoare state
monad contains Hoare triples (precondition, program, postcondition) [11], and
a computation maps an initial state to a pair consisting of a final state and
a returned value. The unit is the monadic operation return, which lifts
returned values into the state monad, and the multiplication is the monadic
operation bind, which composes two computations, passing the resulting state
and returned value of the first computation to the second [27]. The Dijkstra
monad captures functions from postconditions to preconditions [11, 26]. The
return operation gives the weakest precondition of a pure computation, and the
bind operation gives the weakest precondition for a composition of two
computations.

Hoare logic and weakest preconditions are purely assertional proof methods.
Monads combine operational and assertional techniques, since they provide
operations which return the assertions that are used in the correctness
proofs. My approach is purely operational, since it uses no assertions
(formula in a suitable logic) but rather pre- and post-programs instead. My
approach thus represents the operational endpont of the
assertional–operational continuum, with Hoare logic/weakest preconditions at
the other (assertional) endpoint, and monads somewhere in between.

##  9 Conclusions

I have presented a new method for verifying the correctness of sequential
deterministic programs. The method does not use assertions to specify
correctness properties, but rather “specification programs”, which define a
set of “post states”, and can thus replace an assertion, which also defines a
set of states, namely the states that satisfy it. Since specification programs
are not executed, they can be inefficient, and can refer to any mathematically
well-defined quantity, e.g., shortest path distances in a directed graph. In
general, any formula of first/higher order logic can be referenced.

I illustrated my method on three examples: selection sort, Dijkstra’s shortest
path algorithm, and in-place list-reversal. My approach has the following
advantages, as illustrated by the examples:

  * •

_Code synthesis_ : unwinding the outer loop of the pre-program and then
trading it into the program can give initial code for a loop body of the
program. This technique was illustrated in all three examples.

  * •

_Trading_ : trading gives great flexibility in developing both the program and
the pre-program, as code can be freely moved between the program and the pre-
program. This provides a tactic which is not available in logic-based
verification methods such as Floyd-Hoare logic [5, 9] and separation logic
[24]. Trading was used in the sorting and list reversal examples.

  * •

_Separation effect_ : in the in-place list reversal example, a key requirement
is that the reversed part of the list does not link around back to the non-
reversed part. This requirement is easily expressed in my framework by the
pre-program; in particular by how the pre-program constructs the list and then
reverses part of it. Hence, using a pre-program which expresses, in an
operational manner, the needed separation in pointer-based data structures,
achieves the same effect as logic-based methods such as separation logic [24].

  * •

_Refinement_ : use a “coarse” and inefficient specification program and derive
a more efficient program. Now iterate by using this program as a specification
program to derive a still more efficient program, etc. My approach thus
accommodates multi-level refinement.

  * •

_Practical application_ : it may be easier for developers to write
specifications in code, a formalism that they are already well familiar with.

My approach is, to my knowledge, the first which uses _purely_ operational
specifications to verify the correctness of sequential programs, as opposed to
pre- and post-conditions and invariants in a logic such as Floyd-Hoare logic
and separation logic, or axioms and signatures in algebraic specifications
[28]. The use of operational specifications is of course well-established for
the specification and verification of concurrent programs. The process-algebra
approach [7, 15, 16] starts with a specification written in a process algebra
formalism such as CSP, CCS, or the Pi-calculus, and then refines it into an
implementation. Equivalence of the implementation and specification is
established by showing a bisimulation [15, 20] between the two. The I/O
Automata approach [13] starts with a specification given as a single “global
property automaton” and shows that a distributed/concurrent implementation
respects the global property automaton by establishing a simulation relation
[14] from the implementation to the specification.

My approach requires, in some cases, that one establish the equivalence of two
programs [2, 21, 12]. Any method for showing program equivalence works, since
the equivalence is simply the hypothesis for the (Substitution) rule. The
equivalence proofs in this paper were informal and “by inspection”, based on
concepts such as the commutativity of assignment statements that modify
different variables/objects

Future work includes more examples and case studies, and in particular
examples with pointer-based data structures. I am also extending the
operational annotations approach to the verification of concurrent programs.

## References

  * [1] Ralph-Johan Back and Joakim von Wright.  Refinement Calculus - A Systematic Introduction.  Graduate Texts in Computer Science. Springer, 1998.
  * [2] Ştefan Ciobâcă, Dorel Lucanu, Vlad Rusu, and Grigore Rosu.  A language-independent proof system for full program equivalence.  Formal Aspects Comput., 28(3):469–497, 2016.
  * [3] Roy L. Crole and Andrew D. Gordon.  Relating operational and denotational semantics for input/output effects.  Math. Struct. Comput. Sci., 9(2):125–158, 1999.
  * [4] Edsger W. Dijkstra.  Guarded commands, nondeterminacy and formal derivation of programs.  Commun. ACM, 18(8):453–457, August 1975.
  * [5] R Floyd.  Assigning meanings to programs.  In Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics, pages 19–32. American Mathematical Society, 1967.
  * [6] Nissim Francez.  Program verification.  International computer science series. Addison-Wesley, 1992.
  * [7] C. A. R. Hoare.  Communicating Sequential Processes.  Prentice-Hall, 1985.
  * [8] C. A. R. Hoare, Ian J. Hayes, Jifeng He, Carroll Morgan, A. W. Roscoe, Jeff W. Sanders, Ib Holm Sørensen, J. Michael Spivey, and Bernard Sufrin.  Laws of programming.  Commun. ACM, 30(8):672–686, 1987.
  * [9] C.A.R. Hoare.  An axiomatic basis for computer programming.  Communications of the ACM, 12(10):576–580, 583, 1969.
  * [10] Tony Hoare.  Laws of programming: The algebraic unification of theories of concurrency.  In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 1–6. Springer, 2014.
  * [11] Bart Jacobs.  Dijkstra and hoare monads in monadic computation.  Theor. Comput. Sci., 604:30–45, 2015.
  * [12] Dorel Lucanu and Vlad Rusu.  Program equivalence by circular reasoning.  Formal Aspects Comput., 27(4):701–726, 2015.
  * [13] Nancy A. Lynch and Mark R. Tuttle.  An introduction to input/output automata.  CWI-Quarterly, 2(3):219–246, September 1989.  Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands. Technical Memo MIT/LCS/TM-373, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA 02139, November 1988.
  * [14] Nancy A. Lynch and Frits W. Vaandrager.  Forward and backward simulations: I. untimed systems.  Inf. Comput., 121(2):214–233, 1995.
  * [15] Robin Milner.  A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science.  Springer, 1980.
  * [16] Robin Milner.  Communicating and mobile systems - the Pi-calculus.  Cambridge University Press, 1999.
  * [17] Eugenio Moggi.  Computational lambda-calculus and monads.  In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989, pages 14–23. IEEE Computer Society, 1989.
  * [18] Eugenio Moggi.  Notions of computation and monads.  Inf. Comput., 93(1):55–92, 1991.
  * [19] Carroll Morgan.  Programming from specifications, 2nd Edition.  Prentice Hall International series in computer science. Prentice Hall, 1994.
  * [20] David Michael Ritchie Park.  Concurrency and automata on infinite sequences.  In Peter Deussen, editor, Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer, 1981\.
  * [21] Andrew M. Pitts.  Operational semantics and program equivalence.  In Gilles Barthe, Peter Dybjer, Luis Pinto, and João Saraiva, editors, Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, volume 2395 of Lecture Notes in Computer Science, pages 378–412. Springer, 2000.
  * [22] Andrew M. Pitts and Ian David Bede Stark.  Observable properties of higher order functions that dynamically create local names, or what’s new?  In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS’93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 122–141. Springer, 1993.
  * [23] Gordon D. Plotkin.  A structural approach to operational semantics.  J. Log. Algebraic Methods Program., 60-61:17–139, 2004.
  * [24] John C. Reynolds.  Separation logic: A logic for shared mutable data structures.  In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS ’02, pages 55–74, Washington, DC, USA, 2002. IEEE Computer Society.
  * [25] David A. Schmidt.  Programming language semantics.  In Teofilo F. Gonzalez, Jorge Diaz-Herrera, and Allen Tucker, editors, Computing Handbook, Third Edition: Computer Science and Software Engineering, pages 69: 1–19. CRC Press, 2014.
  * [26] Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cedric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Beguelin.  Dependent types and multi-monadic effects in F.  In Rastislav Bodik and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 256–270. ACM, 2016.
  * [27] Wouter Swierstra.  A hoare logic for the state monad.  In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 440–451, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg.
  * [28] Martin Wirsing.  Algebraic specification.  In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 675–788. Elsevier and MIT Press, 1990.