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\}}} } }\]

assume ⟹ assert

\[WP(L:x:=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$

Leave a comment