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

   Author: Jean-Christophe Filliâtre (CNRS)
   Tool:   Why3 (see https://gforge.inria.fr/projects/why3/)
*)
8

9
module SearchingALinkedList
10

11
  use import int.Int
12 13
  use export list.List
  use export list.Length
14
  use export list.Nth
15

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

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

22
  let rec search (i: int) (l: list int) variant { length l } =
23 24 25 26 27
    {}
    match l with
    | Nil -> i
    | Cons x r -> if x = 0 then i else search (i+1) r
    end
Andrei Paskevich's avatar
Andrei Paskevich committed
28 29 30
    { (i <= result < i + length l /\ zero_at l (result - i))
      \/
      (result = i + length l /\ no_zero l) }
31

32
  let search_list (l: list int) =
33 34
    { }
    search 0 l
Andrei Paskevich's avatar
Andrei Paskevich committed
35 36 37
    { (0 <= result < length l /\ zero_at l result)
      \/
      (result = length l /\ no_zero l) }
38 39


40
  (* imperative version, with a loop *)
41

42
  use import module ref.Ref
43 44
  use import list.HdTl

45 46 47 48
  let head (l : list 'a) =
    { l <> Nil }
    match l with Nil -> absurd | Cons h _ -> h end
    { hd l = Some result }
49

50 51 52 53
  let tail (l : list 'a) =
    { l <> Nil }
    match l with Nil -> absurd | Cons _ t -> t end
    { tl l = Some result }
54

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

73 74
end

75
(*
76
Local Variables:
77
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_search_list.gui"
78
End:
79
*)