vstte10_search_list.mlw 1.79 KB
 Jean-Christophe Filliatre committed Jun 22, 2011 1 2 3 4 ``````(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 3: searching a linked list `````` Jean-Christophe Filliatre committed Jul 05, 2011 5 6 `````` Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) `````` Jean-Christophe Filliatre committed Jun 22, 2011 7 ``````*) `````` 8 `````` `````` Jean-Christophe Filliatre committed Jun 21, 2011 9 ``````module SearchingALinkedList `````` Jean-Christophe Filliatre committed Jan 24, 2011 10 `````` `````` Jean-Christophe Filliatre committed Dec 30, 2010 11 `````` use import int.Int `````` Guillaume Melquiond committed Aug 21, 2014 12 13 14 15 `````` use import option.Option use import list.List use import list.Length use import list.Nth `````` Jean-Christophe Filliatre committed Nov 11, 2010 16 `````` `````` Andrei Paskevich committed Jun 29, 2011 17 18 `````` 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 Filliatre committed Nov 11, 2010 19 `````` `````` Andrei Paskevich committed Jun 29, 2011 20 `````` predicate no_zero (l: list int) = `````` Jean-Christophe Filliatre committed Nov 11, 2010 21 `````` forall j:int. 0 <= j < length l -> nth j l <> Some 0 `````` 22 `````` `````` Andrei Paskevich committed Oct 13, 2012 23 24 25 26 `````` let rec search (i: int) (l: list int) variant {l} ensures { (i <= result < i + length l /\ zero_at l (result - i)) \/ (result = i + length l /\ no_zero l) } = match l with `````` Jean-Christophe Filliatre committed May 20, 2011 27 28 29 `````` | Nil -> i | Cons x r -> if x = 0 then i else search (i+1) r end `````` 30 `````` `````` Andrei Paskevich committed Oct 13, 2012 31 32 33 34 `````` let search_list (l: list int) ensures { (0 <= result < length l /\ zero_at l result) \/ (result = length l /\ no_zero l) } = search 0 l `````` 35 36 `````` `````` Jean-Christophe Filliatre committed May 20, 2011 37 `````` (* imperative version, with a loop *) `````` Jean-Christophe Filliatre committed Nov 15, 2010 38 `````` `````` Andrei Paskevich committed Oct 13, 2012 39 `````` use import ref.Ref `````` Jean-Christophe Filliatre committed Nov 15, 2010 40 41 `````` use import list.HdTl `````` Andrei Paskevich committed Oct 13, 2012 42 43 44 `````` let head (l : list 'a) requires { l <> Nil } ensures { hd l = Some result } = match l with Nil -> absurd | Cons h _ -> h end `````` Jean-Christophe Filliatre committed Nov 15, 2010 45 `````` `````` Andrei Paskevich committed Oct 13, 2012 46 47 48 `````` let tail (l : list 'a) requires { l <> Nil } ensures { tl l = Some result } = match l with Nil -> absurd | Cons _ t -> t end `````` Jean-Christophe Filliatre committed Nov 15, 2010 49 `````` `````` Andrei Paskevich committed Oct 13, 2012 50 51 52 53 `````` let search_loop l ensures { (0 <= result < length l /\ zero_at l result) \/ (result = length l /\ no_zero l) } = let i = ref 0 in `````` Jean-Christophe Filliatre committed May 20, 2011 54 55 56 `````` let s = ref l in while !s <> Nil && head !s <> 0 do invariant { `````` Andrei Paskevich committed Jun 29, 2011 57 58 `````` 0 <= !i /\ !i + length !s = length l /\ (forall j:int. 0 <= j -> nth j !s = nth (!i + j) l) /\ `````` Jean-Christophe Filliatre committed May 20, 2011 59 `````` forall j:int. 0 <= j < !i -> nth j l <> Some 0 } `````` Andrei Paskevich committed Oct 13, 2012 60 `````` variant { !s } `````` Jean-Christophe Filliatre committed May 20, 2011 61 62 63 64 `````` i := !i + 1; s := tail !s done; !i `````` Jean-Christophe Filliatre committed Nov 15, 2010 65 `````` `````` Jean-Christophe Filliatre committed Dec 29, 2010 66 ``end``