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

5 6
  use import int.Int
  use import module stdlib.Ref
7 8
  use export list.List
  use export list.Length
9
  use export list.Nth
10 11 12 13 14 15

  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
16

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

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


35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
(* 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 { 
55 56 57 58
      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 }
59 60 61 62 63 64 65 66
    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) }

67 68
end

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