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

{
  use export list.List
  use export list.Length
7
  use export list.Nth
8 9 10 11 12 13

  logic zero_at (l : list int) (i : int) =
    nth i l = Some 0 and forall j:int. 0 <= j < i -> nth j l <> Some 0 

  logic no_zero (l : list int) =
    forall j:int. 0 <= j < length l -> nth j l <> Some 0
14 15
}

16
let rec search i l variant { length l } = 
17
  {}
18 19 20 21
  match l with
  | Nil -> i
  | Cons x r -> if x = 0 then i else search (i+1) r
  end
22
  { (i <= result < i + length l and zero_at l (result - i)) 
23
    or
24
    (result = i + length l and no_zero l) }
25 26 27 28

let search_list l =
  { }
  search 0 l
29
  { (0 <= result < length l and zero_at l result)
30
    or 
31
    (result = length l and no_zero l) }
32 33


34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
(* imperative version, with a loop *)

{
  use import list.HdTl
}

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

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

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

68 69 70 71 72
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_search_list.gui"
End: 
*)