Why3 group



Links

Set-up

On debian unstable, with opam and ocaml already installed.
Install system dependencies, Z3 and CVC4: 
sudo apt install libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev zlib1g-dev libgmp-dev pkg-config autoconf z3 cvc4
Install opam dependencies and alt-ergo: 
opam install ocamlfind menhir num zarith camlzip ocamlgraph lablgtk3 lablgtk3-sourceview3 re alt-ergo
Clone the repository: 
git clone https://gitlab.inria.fr/why3/why3.git
Build Why3: 
cd why3 && ./autogen.sh && ./configure && make
Install Why3: 
sudo make install
Detect installed provers and generate configuration file: 
why3 config detect
Test your installation: 
cd examples && why3 ide -L . mergesort_array.mlw

Tutorial

Taken from An introduction to deductive program verification.

Factorial recursive

Prove soundness and termination.
module FactRecursive

  use int.Int
  use int.Fact

  let rec fact_rec (n: int) : int
    requires { true }
    ensures  { result = fact n }
  =
    if n = 0 then 1
    else n * fact_rec (n - 1)

end
mkdir fact && cd fact && why3 ide -L . factrecursive.mlw
Select the goal 
fact_rec'vc
and press S to split the goal.
Then select the new 
split_vc
goal and press 0 to run provers on all its subgoals.
After making a change, press Ctrl + R to update the goals.
module FactRecursive

  use int.Int
  use int.Fact

  let rec fact_rec (n: int) : int
    requires { n >= 0 }
    variant  { n }
    ensures  { result = fact n }
  =
    if n = 0 then 1
    else n * fact_rec (n - 1)

  let test0 () = fact_rec 0
  let test1 () = fact_rec 1
  let test7 () = fact_rec 7
  let test42 () = fact_rec 42

end

Factorial imperative

Prove soundness, termination and change the code to use a for loop instead of a while loop.
module FactImperative

  use int.Int
  use int.Fact
  use ref.Ref

  let fact_imp (n: int) : int
    requires { true }
    ensures  { result = fact n }
  =
    let ref m = 0 in
    let ref r = 1 in
    while m < n do
      invariant { true }
      m := m + 1;
      r := r * m
    done;
    r

end
You can use 
let ref x = e
and avoid having to dereference it or 
let x = ref e
and use the classical 
!x
to get its value.
module FactImperative

  use int.Int
  use int.Fact
  use ref.Ref

  let fact_imp (n: int) : int
    requires { n >= 0 }
    ensures { result = fact n }
  =
    let ref m = 0 in
    let ref r = 1 in
    while m < n do
      invariant { 0 <= m <= n }
      invariant { r = fact m }
      variant { n - m }
      m := m + 1;
      r := r * m
    done;
    r

  let test0 () = fact_imp 0
  let test1 () = fact_imp 1
  let test7 () = fact_imp 7
  let test42 () = fact_imp 42

end

Queue module

Taken from (don't look now, the solution is there) Why3 gallery.
Write a complete specification, fill the implementation and prove it. 
module Queue

  use int.Int
  use mach.peano.Peano
  use list.List
  use list.Length
  use list.Reverse
  use list.NthNoOpt
  use list.Append
  use seq.Seq
  use seq.FreeMonoid

  type t 'a = {
    mutable front: list 'a; (* entry *)
    mutable rear: list 'a;  (* exit *)
    ghost mutable seq: Seq.seq 'a;
  }
    invariant { true }

  meta coercion function seq

  let create () : t 'a
    ensures { true }
  = {
    front = Nil;
    rear = Nil;
    seq = empty
  }

  let push (x: 'a) (q: t 'a) : unit
    writes  {  }
    ensures { true }
  =
    ()

  exception Empty

  let pop (q: t 'a) : 'a
    writes  {  }
    ensures { true }
    raises  { Empty  }
  =
    raise Empty

  let peek (q: t 'a) : 'a
    ensures { true }
    raises  { Empty }
  =
    raise Empty

  let safe_pop (q: t 'a) : 'a
    requires { true }
    writes {  }
    ensures { true }
  =
    try pop q with Empty -> absurd end

  let safe_peek (q: t 'a) : 'a
    requires { true }
    ensures { true }
  =
    try peek q with Empty -> absurd end

  let clear (q: t 'a) : unit
    writes {  }
    ensures { true }
  =
    ()

  let copy (q: t 'a) : t 'a
    ensures { true }
  =
    q

  let is_empty (q: t 'a)
    ensures { true }
  =
    true

  let length (q: t 'a) : Peano.t
    ensures { true }
  =
    Peano.zero

  let transfer (q1: t 'a) (q2: t 'a) : unit
    writes  {  }
    ensures { true }
  =
    ()

end

module Queue

  use int.Int
  use mach.peano.Peano
  use list.List
  use list.Length
  use list.Reverse
  use list.NthNoOpt
  use list.Append
  use seq.Seq
  use seq.FreeMonoid

  type t 'a = {
    mutable front: list 'a; (* entry *)
    mutable rear: list 'a;  (* exit *)
    ghost mutable seq: Seq.seq 'a;
  }
    invariant { length seq = Length.length front + Length.length rear }
    invariant { Length.length front > 0 -> Length.length rear > 0 }
    invariant {
      forall i. 0 <= i < length seq ->
        seq[i] =
          let n = Length.length rear in
          if i < n then nth i rear
          else nth (Length.length front - 1 - (i - n)) front }

  meta coercion function seq

  let create () : t 'a
    ensures { result = empty }
  = {
    front = Nil;
    rear = Nil;
    seq = empty
  }

  let push (x: 'a) (q: t 'a) : unit
    writes  { q }
    ensures { q = snoc (old q) x }
  = match q.front, q.rear with
    | Nil, Nil -> q.rear <- Cons x Nil
    | _        -> q.front <- Cons x q.front
    end;
    q.seq <- snoc q.seq x

  let rec lemma nth_append (i: int) (l1: list 'a) (l2: list 'a)
    requires { 0 <= i < Length.length l1 + Length.length l2 }
    ensures {
      nth i (Append.(++) l1 l2) =
      if i < Length.length l1 then nth i l1
      else nth (i - Length.length l1) l2 }
    variant { l1 }
  =
    match l1 with
    | Nil -> ()
    | Cons _ r1 ->
      if i > 0 then nth_append (i - 1) r1 l2
    end

  let rec lemma nth_rev (i: int) (l: list 'a)
    requires { 0 <= i < Length.length l }
    ensures { nth i l = nth (Length.length l - 1 - i) (reverse l) }
    variant { l }
  =
    match l with
    | Nil -> absurd
    | Cons _ s ->
      if i > 0 then nth_rev (i - 1) s
    end

  exception Empty

  let pop (q: t 'a) : 'a
    writes  { q }
    ensures { (old q) <> empty }
    ensures { result = (old q)[0] }
    ensures { q = (old q)[1 ..] }
    raises  { Empty -> q = old q = empty }
  =
    let res = match q.rear with
      | Nil -> raise Empty
      | Cons x Nil -> q.front, q.rear <- Nil, reverse q.front; x
      | Cons x s -> q.rear <- s; x
      end in
    q.seq <- q.seq [1 ..];
    res

  let peek (q: t 'a) : 'a
    ensures { q <> empty }
    ensures { result = q[0] }
    raises  { Empty -> q == empty }
  =
    match q.rear with
    | Nil -> raise Empty
    | Cons x _ -> x
    end

  let safe_pop (q: t 'a) : 'a
    requires { q <> empty }
    writes { q }
    ensures { result = (old q)[0] }
    ensures { q = (old q)[1 ..] }
  = try pop q with Empty -> absurd end

  let safe_peek (q: t 'a) : 'a
    requires { q <> empty }
    ensures { result = q[0] }
  = try peek q with Empty -> absurd end

  let clear (q: t 'a) : unit
    writes { q }
    ensures { q = empty }
  =
    q.seq <- empty;
    q.rear <- Nil;
    q.front <- Nil

  let copy (q: t 'a) : t 'a
    ensures { result == q }
  = {
    front = q.front;
    rear = q.rear;
    seq = q.seq
    }

  let is_empty (q: t 'a)
    ensures { result <-> q == empty }
  =
    match q.front, q.rear with
    | Nil, Nil -> true
    | _ -> false
    end

  let length (q: t 'a) : Peano.t
    ensures { result = Seq.length q.seq }
  =
    let rec length_aux (acc: Peano.t) (l: list 'a) : Peano.t
      ensures { result = acc + Length.length l }
      variant { l }
    = match l with
    | Nil -> acc
    | Cons _ s -> length_aux (Peano.succ acc) s
    end in
    length_aux (length_aux Peano.zero q.front) q.rear

  let transfer (q1: t 'a) (q2: t 'a) : unit
    writes  { q1, q2 }
    ensures { q1 = empty }
    ensures { q2 = (old q2) ++ (old q1) }
  = match q2.rear with
    | Nil ->
      q2.front, q2.rear, q2.seq <- q1.front, q1.rear, q1.seq
    | _ ->
      q2.front <- Append.(++) q1.front (Append.(++) (reverse q1.rear) q2.front);
      q2.seq <- q2.seq ++ q1.seq;
    end;
    clear q1

end