Forward Reasoning

• Suppose we initially know (or assume) that $w > 0$

// w > 0
x := 17;
// w > 0 and x = 17
y := 42;
// w > 0 and x = 17 and y = 42
z := w + x + y
// w > 0 and x = 17 and y = 42 and z > 59

• Then we can deduce a few facts about the resulting state (e.g. $z > 59$)

Backward Reasoning

• Suppose we want $z < 0$ at the end

// w + 17 + 42 < 0
x := 17;
// w + x + 42 < 0
y := 42;
// w + x + y < 0
z := w + x + y
// z < 0

• Then the initial state must satisfy $w < -59$

Side Note: Forward Assignment

• Note that the Assignment Axiom that we introduce works backwards: $$ \izero{Asgn}{\ht{\subst{Q}{x}{E}}{x:=E}{Q}} $$
• This naturally raises the question: how could we formulate a forward version of this axiom?

Side Note: Forward Assignment

• Based on our examples, perhaps the following can be used? $$ \izero{AgFw}{\ht{P}{x:=E}{P \,\wedge\, x=E}} $$
• Example: $\scriptsize\ht{w > 0}{x:=17}{w>0 \wedge x=17}$
• No! Example: $\scriptsize\ht{w > 0}{x:=x+1}{w>0 \wedge x=x+1}$

Side Note: Forward Assignment

• What about the following rule? $$ \izero{AgFw}{\ht{P}{x:=E}{\subst{P}{x}{E}}} $$
• No! Example: $\scriptsize\ht{x=0}{x:=1}{1=0}$
• It's easy to check that if we use $\subst{P}{E}{x}$, similar problems arise.

Side Note: Forward Assignment

• We can use the following rule, due to Floyd: $$ \izero{AgFw}{\ht{P}{x:=E}{\exists v \cdot x=\subst{E}{x}{v} \wedge \subst{P}{x}{v}}} $$
• Example: $\scriptsize\ht{x=0}{x:=1}{\exists v \cdot x=1 \wedge v=0}$
• Backward and forward rules are equivalent, but it is more difficult to use the forward rule (we have to find the variable $v$).

Side Note: Forward Assignment

• The previous discussion shows that it is easy to have wrong intuitions about the assignment axiom.
• This shows the importance of having a rigorous means of establishing the validity of axioms and rules.
• We can define a formal semantics for our language and then prove that the axioms and rules are sound.

Forward vs Backward Reasoning

• Forward Reasoning is more intuitive for most people
  • Helps in understanding what follows from initial assumptions
  • Useful for ensuring that an invariant is mantained
  • However, it might introduce irrelevant facts
• Backward Reasoning is usually more helpful
  • Helps in understanding what should happen
  • Crucial in Program Derivation!

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)}\\ = & 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 and boring (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

The general approach for Hoare-style formal verification:

• A programmer annotates source code
• A tool analyses the code and attempts to show that all the assertions given can be derived using the rules of Hoare Logic
• The tool may be able to do this unassisted
• If not, it emits verification conditions, purely logical assertions that need to be checked
• These may be passed on to an automated theorem prover, or some other decision procedure
• 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

Dafny

• Programming language designed for reasoning
• Language features drawn from:
  • Imperative programming: if, while, :=, class, ...
  • Functional programming: function, datatype, codatatype, ...
  • Proof authoring: Lemma, calc, refines, inductive predicate, ...

Dafny is aimed at reasoning

Dafny's Architecture

• Dafny uses Boogie as an intermediate verification language
• The generation of verification conditions occurs at the Boogie level
• The generated conditions are then checked by an external solver / theorem prover