Wiki Agenda Contact Version française

Searching a Linked List, in Why3

Searching the index of the first occurrence of 0 in a linked list of integers, Why3 version


Authors: Jean-Christophe Filliâtre

Topics: List Data Structure / Searching Algorithms

Tools: Why3

References: The 1st Verified Software Competition / The VerifyThis Benchmarks

see also the index (by topic, by tool, by reference, by year)


(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 3: searching a linked list

   Author: Jean-Christophe Filliatre (CNRS)
   Tool:   Why3 (see http://why3.lri.fr/)
*)

module SearchingALinkedList

  use import int.Int
  use import option.Option
  use import list.List
  use import list.Length
  use import list.Nth

  predicate zero_at (l: list int) (i: int) =
    nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0

  predicate no_zero (l: list int) =
    forall j:int. 0 <= j < length l -> nth j l <> Some 0

  let rec search (i: int) (l: list int) variant {l}
    ensures { (i <= result < i + length l /\ zero_at l (result - i)) \/
              (result = i + length l /\ no_zero l) }
  = match l with
    | Nil -> i
    | Cons x r -> if x = 0 then i else search (i+1) r
    end

  let search_list (l: list int)
    ensures { (0 <= result < length l /\ zero_at l result) \/
              (result = length l /\ no_zero l) }
  = search 0 l

  (* imperative version, with a loop *)

  use import ref.Ref
  use import list.HdTl

  let head (l : list 'a)
    requires { l <> Nil } ensures { hd l = Some result }
  = match l with Nil -> absurd | Cons h _ -> h end

  let tail (l : list 'a)
    requires { l <> Nil } ensures { tl l = Some result }
  = match l with Nil -> absurd | Cons _ t -> t end

  let search_loop l
    ensures { (0 <= result < length l /\ zero_at l result) \/
              (result = length l /\ no_zero l) }
  = let i = ref 0 in
    let s = ref l in
    while !s <> Nil && head !s <> 0 do
      invariant {
        0 <= !i /\ !i + length !s = length l /\
        (forall j:int. 0 <= j -> nth j !s = nth (!i + j) l) /\
        forall j:int. 0 <= j < !i -> nth j l <> Some 0 }
      variant { !s }
      i := !i + 1;
      s := tail !s
    done;
    !i

end

download ZIP archive

Why3 Proof Results for Project "vstte10_search_list"

Theory "vstte10_search_list.SearchingALinkedList": fully verified in 3.29 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)Coq (8.4pl6)Z3 (3.2)
VC for search0.07---------
VC for search_list0.010.00---0.00
VC for head0.000.01---0.01
VC for tail0.020.01---0.02
VC for search_loop------------
split_goal_wp
  1. loop invariant init0.010.01---0.00
2. precondition0.010.01---0.00
3. precondition0.010.01---0.02
4. loop invariant preservation------------
split_goal_wp
  1. VC for search_loop0.010.02---0.02
2. VC for search_loop0.020.02---0.02
3. VC for search_loop------0.88---
4. VC for search_loop------1.04---
5. loop variant decrease0.010.01------
6. postcondition------0.96---
7. postcondition0.010.02---0.02