Decorated Programs

• Doing proofs in Hoare Logic can feel overly verbose
• Decorating programs is a way to informally write down a Hoare Logic proof
  • The idea is to insert assertions between every construct that makes the program. For example:

Decorated Programs: Skip and Assignment

Decorated Programs: Sequential Composition and While loops

Decorated Programs: Conditionals and Consequence rules

Example: A decorated program

Verify the following program by decorating it:

Verify the following program by decorating it:

Invariants

• To reason about loops, we need to identify loop invariants, which might be difficult!
• For example, $\scriptsize j\ge 1$ is an invariant of the loop: $$\scriptsize i:=1;\,j:=1;\,\whileloop{i\lt n}{j:=j{+}i;\,i:=i{+}1}$$ but we cannot prove $$\scriptsize \ht{j\ge 1 \,\wedge\, i\lt n}{j:=j{+}i;\,i:=i{+}1}{j\ge 1}$$
• We need to strengthen the invariant: $\scriptsize j\ge 1 \,\wedge\, i\ge 1$

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.

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