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

4 5
module M

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

  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
17

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

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


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

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