vstte10_search_list.mlw 1.63 KB
Newer Older
1
module M
2
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
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
let rec search i l variant { length l } = 
16
  {}
17 18 19 20
  match l with
  | Nil -> i
  | Cons x r -> if x = 0 then i else search (i+1) r
  end
21
  { (i <= result < i + length l and zero_at l (result - i)) 
22
    or
23
    (result = i + length l and no_zero l) }
24 25 26 27

let search_list l =
  { }
  search 0 l
28
  { (0 <= result < length l and zero_at l result)
29
    or 
30
    (result = length l and no_zero l) }
31 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
(* 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) }

65 66
end

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