vstte10_search_list.mlw 856 Bytes
 1 2 3 4 5 6 ``````(* VSTTE'10 competition Problem 3: searching a linked list *) { use export list.List use export list.Length `````` Jean-Christophe Filliâtre committed Nov 10, 2010 7 `````` use export list.Nth `````` 8 9 10 ``````} let rec search i l = `````` Jean-Christophe Filliâtre committed Nov 10, 2010 11 `````` {} `````` 12 13 14 15 `````` match l with | Nil -> i | Cons x r -> if x = 0 then i else search (i+1) r end `````` Jean-Christophe Filliâtre committed Nov 10, 2010 16 17 18 19 20 `````` { (i <= result < i + length l and nth (result - i) l = Some 0 and forall j:int. 0 <= j < result - i -> nth j l <> Some 0) or (result = i + length l and forall j:int. 0 <= j < length l -> nth j l <> Some 0) } `````` 21 22 23 24 `````` let search_list l = { } search 0 l `````` Jean-Christophe Filliâtre committed Nov 10, 2010 25 26 27 28 29 `````` { (0 <= result < length l and nth result l = Some 0 and forall j:int. 0 <= j < result -> nth j l <> Some 0) or (result = length l and forall j:int. 0 <= j < length l -> nth j l <> Some 0) } `````` 30 31 32 33 34 35 36 `````` (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_search_list.gui" End: *)``````