vstte10_search_list.mlw 1.79 KB
Newer Older
1 2 3 4
(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 3: searching a linked list

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

9
module SearchingALinkedList
10

11
  use import int.Int
12 13 14 15
  use import option.Option
  use import list.List
  use import list.Length
  use import list.Nth
16

Andrei Paskevich's avatar
Andrei Paskevich committed
17 18
  predicate zero_at (l: list int) (i: int) =
    nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0
19

Andrei Paskevich's avatar
Andrei Paskevich committed
20
  predicate no_zero (l: list int) =
21
    forall j:int. 0 <= j < length l -> nth j l <> Some 0
22

23 24 25 26
  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
27 28 29
    | Nil -> i
    | Cons x r -> if x = 0 then i else search (i+1) r
    end
30

31 32 33 34
  let search_list (l: list int)
    ensures { (0 <= result < length l /\ zero_at l result) \/
              (result = length l /\ no_zero l) }
  = search 0 l
35 36


37
  (* imperative version, with a loop *)
38

39
  use import ref.Ref
40 41
  use import list.HdTl

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

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

50 51 52 53
  let search_loop l
    ensures { (0 <= result < length l /\ zero_at l result) \/
              (result = length l /\ no_zero l) }
  = let i = ref 0 in
54 55 56
    let s = ref l in
    while !s <> Nil && head !s <> 0 do
      invariant {
Andrei Paskevich's avatar
Andrei Paskevich committed
57 58
        0 <= !i /\ !i + length !s = length l /\
        (forall j:int. 0 <= j -> nth j !s = nth (!i + j) l) /\
59
        forall j:int. 0 <= j < !i -> nth j l <> Some 0 }
60
      variant { !s }
61 62 63 64
      i := !i + 1;
      s := tail !s
    done;
    !i
65

66
end