Program Derivation

• Usually, in practice, we start with a specification of what we need to implement
  • Example: "develop an algorithm that sorts an array of integers"
• The axioms and rules of Hoare Logic can help us guide the development process.
  • Edsger W. Dijkstra was one of the pioneers of formal program derivation (aka program calculation)

First example: Multiple Assignments

• Calculate non-zero $A$ and $B$ such that: $$\scriptsize\ht{x+y=M}{x,y := x+A,y+B}{x+y=M}$$
• Using the assignment axiom, we have $$\scriptsize\ht{(x+A)+(y+B)=M}{x,y := x+A,y+B}{x+y=M}$$
• We thus need to calculate non-zero $A$ and $B$ such that $\,\,\,\,\,\scriptsize x+y=M \,\,\rightarrow\,\,(x+A)+(y+B)=M$

First example: Multiple Assignments

• We thus need to calculate non-zero $A$ and $B$ such that $\,\,\,\,\,\scriptsize x+y=M \,\,\rightarrow\,\,(x+A)+(y+B)=M$
• A possible calculation is: $$\scriptsize \begin{array}{llr} & (x+A)+(y+B)=M &\\ = & (x+y)+(A+B)=M & \textrm{(associativity and symmetry)}\\ = & M +(A+B)=M & \textrm{(assumption $x+y=M$)}\\ = & A+B = 0 & \textrm{(arithmetic)}\\ \leftarrow & A=1 \wedge B=-1 & \textrm{(strengthening)}\\ \end{array} $$

First example: Multiple Assignments

• We thus have: $$\scriptsize\ht{x+y=M}{x,y := x+1,y-1}{x+y=M}$$
• We could have made other choices for $A$ and $B$, but the main point is that we did not guess what the assignments would be: instead, we calculated them.

A useful programming technique

• Suppose that we want to develop an algorithm that establishes $P \wedge Q$. One way achieving this is to find some command $C$ such that: $$ \ht{P}{\whileloop{\neg{Q}}{C}}{P \wedge Q} $$
• In words: we choose one of the conjuncts for the loop invariant and the negation of the other for the loop condition.

Exercise (Integer Division)

Calculate an algorithm that takes two positive numbers $A$ and $B$ and computes $A \div B$ (quotient) and $A \bmod B$ (remainder).

Obviously, we assume that these operators are not available in our language. Let's assume we only have addition and subtraction available.

(PDF slides with incremental solution)

Exercise (Exponentiation)

Calculate an algorithm that takes two natural numbers $A$ and $B$ and computes $A^B$. More formally:

$$ \ht{A\ge 0 \,\,\wedge\,\, B\ge 0}{\,\,\textrm{Compute $r$}\,\,}{r = A^B} $$

Your algorithm should use addition and multiplication.

Scaling up Hoare-Style Verification

After a few exercises, two problems are clear:

• Proofs are quite long (even for simple programs)
• Proofs involve lots of trivial details (e.g. 3=3 is true)
• Solution: automation!
  • Note: Logicians have shown that is is impossible to design a decision procedure to decide automatically the truth or falsehood of an arbitrary mathematical statement. This means that we cannot prove everything automatically. But, still, we can have procedures that can prove many useful theorems. The goal of a automated verification system is to automate the boring parts.

Hoare Logic in verification tools

General approach for Hoare-style formal verification:

1. A programmer annotates the source code
2. A tool analyses the annotated code and attempts to show that all the assertions given can be derived using the rules of Hoare Logic
3. The tool may be able to do this unassisted
4. If not, it emits verification conditions, purely logical assertions that need to be checked
5. These may be passed on to an automated theorem prover, or some other decision procedure
6. In extreme cases verification conditions may not be solved automatically and require interactive theorem proving by an expert or the provision of extra hints

Verification Conditions from Annotated Programs

To prove $\ht{P}{C}{Q}$, three things must be done:

1. The program $C$ is annotated by inserting into it assertions, expressing conditions that are meant to hold at various intermediate points
2. A set of logic statements called verification conditions is generated from the annotated specification
3. The verification conditions are proved

Annotated Programs

A program is said to be properly annotated if statements have been inserted in the following places:

1. Before each command $C_i$ (where $i\gt 1$) in a sequence $C_1; C_2; \cdots; C_n$ which is not an assignment command
2. As invariant of the while loop

Verification Condition Generator

We can define a recursive procedure to generate verification conditions for an annotated partial correctness specification $\ht{P}{C}{Q}$

We will now see some rules and implement them. We will use Haskell, but you are invited to replicate this exercise using your favourite programming language.

Assignment

Example: $\,\ht{X=0}{X := X+1}{X=1}$ yields $X=0\,\,\rightarrow\,\,(X+1)=1$

Conditionals

The verification conditions generated from $$\ht{P}{\ifthenelse{b}{C1}{C2}}{Q}$$ are:

• The verification conditions of $\ht{P \wedge b}{C1}{Q}$
• The verification conditions of $\ht{P \wedge \neg{b}}{C2}{Q}$

Sequential Composition

We'll define two cases. First, assuming $C_n$ is not an assignment, the verification conditions generated from

are:

• $\ht{P}{C_1; \cdots ;C_{n-1}}{R}$
• $\ht{R}{C_n}{Q}$

Sequential Composition

Second, the verification conditions generated from

are the verification conditions of

While loops

The verification conditions generated from

are

• $P \rightarrow I$
• $I \wedge \neg{b} \rightarrow Q$
• The verification conditions of $\ht{I \wedge b}{C}{I}$

Mini-VCGEN

• We have now implemented a mini (primitive) verification condition generator
• The strategy is to go directly from an annotated program to a list of verification conditions
• Program verifiers such as Dafny follow a different strategy: they "compile" into an intermediate verification language