vstte10_search_list.mlw 1.89 KB
 Jean-Christophe Filliâtre committed Jun 22, 2011 1 2 3 4 5 6 7 ``````(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 3: searching a linked list Author: Jean-Christophe Filliâtre (CNRS) Tool: Why3 (see https://gforge.inria.fr/projects/why3/) *) `````` 8 `````` `````` Jean-Christophe Filliâtre committed Jun 21, 2011 9 ``````module SearchingALinkedList `````` Jean-Christophe Filliâtre committed Jan 24, 2011 10 `````` `````` Jean-Christophe Filliâtre committed Dec 30, 2010 11 `````` use import int.Int `````` 12 13 `````` use export list.List use export list.Length `````` Jean-Christophe Filliâtre committed Nov 10, 2010 14 `````` use export list.Nth `````` Jean-Christophe Filliâtre committed Nov 11, 2010 15 `````` `````` Andrei Paskevich committed Jun 29, 2011 16 17 `````` predicate zero_at (l: list int) (i: int) = nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0 `````` Jean-Christophe Filliâtre committed Nov 11, 2010 18 `````` `````` Andrei Paskevich committed Jun 29, 2011 19 `````` predicate no_zero (l: list int) = `````` Jean-Christophe Filliâtre committed Nov 11, 2010 20 `````` forall j:int. 0 <= j < length l -> nth j l <> Some 0 `````` 21 `````` `````` Jean-Christophe Filliâtre committed Jun 21, 2011 22 `````` let rec search (i: int) (l: list int) variant { length l } = `````` Jean-Christophe Filliâtre committed May 20, 2011 23 24 25 26 27 `````` {} match l with | Nil -> i | Cons x r -> if x = 0 then i else search (i+1) r end `````` Andrei Paskevich committed Jun 29, 2011 28 29 30 `````` { (i <= result < i + length l /\ zero_at l (result - i)) \/ (result = i + length l /\ no_zero l) } `````` 31 `````` `````` Jean-Christophe Filliâtre committed Jun 21, 2011 32 `````` let search_list (l: list int) = `````` Jean-Christophe Filliâtre committed May 20, 2011 33 34 `````` { } search 0 l `````` Andrei Paskevich committed Jun 29, 2011 35 36 37 `````` { (0 <= result < length l /\ zero_at l result) \/ (result = length l /\ no_zero l) } `````` 38 39 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 40 `````` (* imperative version, with a loop *) `````` Jean-Christophe Filliâtre committed Nov 15, 2010 41 `````` `````` Jean-Christophe Filliâtre committed Jun 21, 2011 42 `````` use import module ref.Ref `````` Jean-Christophe Filliâtre committed Nov 15, 2010 43 44 `````` use import list.HdTl `````` Jean-Christophe Filliâtre committed May 20, 2011 45 46 47 48 `````` let head (l : list 'a) = { l <> Nil } match l with Nil -> absurd | Cons h _ -> h end { hd l = Some result } `````` Jean-Christophe Filliâtre committed Nov 15, 2010 49 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 50 51 52 53 `````` let tail (l : list 'a) = { l <> Nil } match l with Nil -> absurd | Cons _ t -> t end { tl l = Some result } `````` Jean-Christophe Filliâtre committed Nov 15, 2010 54 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 55 56 57 58 59 60 `````` let search_loop l = {} let i = ref 0 in let s = ref l in while !s <> Nil && head !s <> 0 do invariant { `````` Andrei Paskevich committed Jun 29, 2011 61 62 `````` 0 <= !i /\ !i + length !s = length l /\ (forall j:int. 0 <= j -> nth j !s = nth (!i + j) l) /\ `````` Jean-Christophe Filliâtre committed May 20, 2011 63 64 65 66 67 68 `````` forall j:int. 0 <= j < !i -> nth j l <> Some 0 } variant { length !s } i := !i + 1; s := tail !s done; !i `````` Andrei Paskevich committed Jun 29, 2011 69 70 71 `````` { (0 <= result < length l /\ zero_at l result) \/ (result = length l /\ no_zero l) } `````` Jean-Christophe Filliâtre committed Nov 15, 2010 72 `````` `````` Jean-Christophe Filliâtre committed Dec 29, 2010 73 74 ``````end `````` 75 ``````(* `````` Jean-Christophe Filliâtre committed May 20, 2011 76 ``````Local Variables: `````` 77 ``````compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_search_list.gui" `````` Jean-Christophe Filliâtre committed May 20, 2011 78 ``````End: `````` 79 ``*)``