vstte10_search_list.mlw 901 Bytes
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


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