# Proof of programs with Why3

Teacher: François Bobot

Different approaches to verification:

• model checking
• astract interpretation
• deductive verification (SAT solving)

Two kinds of verifications:

• ensuring safety

• no false positive (when it says there’s no problem, you’re sure of it)
• bug finding:

• e.g. on github: automatic bug finding

Sucess stories:

• metro in Paris: line A is nowadays completely automatic. At the beginning, the programming was hand-made, but it was very buggy. But today: uses refinement ⟶ automatically verified

• Astrée project (used for flight control)

• Compcert: certified C complier (with Coq)

• this compiler is not as good as gcc is 0.3, but definitely better than it in earlier versions ⟶ used by Airbus nowadays
• EDF (in France) use Frama-C Eva, Airbus use Frama-C WP, etc…
• Airbus is already ensuring that their code is bug-free (because it’s really critical), but verification tools help to check everything automatically, which curb costs
• Spark2014: verifies a subset of Ada programs

# Hoare logic

Will be replaced at the end of the course by something more modern

## Expressions

e ::= n (integer constants)
| x (variables)
| e op e


Integers, variables, binary operations

op ::= + | − | ∗
| = | ≠ | < | > | ≤ | ≥
| and | or

Statements:
  s ::= skip (no effect)
| x := e (assignment)
| s ; s (sequence)
| if e then s else s (conditional)
| while e do s (loop)


Example of a program computing the square root:

count := 0; sum := 1;
while sum ≤ n do
count := count + 1; sum := sum + 2 * count + 1


To express formal properties: first-order logic

$p ::= e \; \mid \; p ∧ p \; \mid \; p ∨ p \; \mid \; ¬p \; \mid \; p ⇒ p \; \mid \; ∀v, p \; \mid \; ∃v, p$
Hoare triples:

Precondition followed by a program s and a postcondition: $\{P\}s\{Q\}$

Examples:

{x = 1}x := x + 2{x = 3}
{x = y}x := x + y{x = 2 ∗ y}
{true}while 1 do skip{false}


or for the square root (actually: integer part of $\sqrt{n}$) program:

{n ≥ 0}ISQRT{count² ≤ n ∧ n < (count + 1)²}


$\cfrac{}{\{P[x ⟻ e]\} x:=e \{P\}}$

or

$\cfrac{}{\{P\} x:=e \{∃ v \; P[x ⟻ v]\}}$

Often, the postcondition gives you a hint as to what the invariant of a loop should be.

$\infer{\{P\} x := e \{∃v; e[x ← v] = x ∧ P[x ← v]\}}{ \infer{\vdots }{ \infer{\{P[x ← e]\} x:=e \{P\}}{\phantom{\{P[x ← e]\} x:=e \{P\}}} } }$

assumeassert

$WP(L=x+42, x@Here > x@L) = WP(x:=x+42, x@Here > x@L)[⋯]\\ = (x@Here+42 > x@L)[⋯]\\ = (x@Here+42 > x@Here)$
Frame property:

if you have $\lbrace P \rbrace C \lbrace Q \rbrace$ and $R$ is a property not modified by $C$, then you have $\lbrace P ∧ R \rbrace C \lbrace Q ∧ R \rbrace$

Tags:

Updated: