coincidence_count_list.mlw 2.65 KB
 Jean-Christophe Filliâtre committed Mar 29, 2016 1 2 3 4 5 6 7 8 9 10 `````` (** Coincidence count Exercise proposed by Rustan Leino at Dagstuhl seminar 16131, March 2016 You are given two sequences of integers, sorted in increasing order and without duplicate elements, and you count the number of elements that appear in both sequences (in linear time and constant space). `````` Jean-Christophe Filliâtre committed Mar 29, 2016 11 `````` See also coincidence_count.mlw for a version using arrays. `````` Jean-Christophe Filliâtre committed Mar 29, 2016 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 `````` Authors: Jean-Christophe Filliâtre (CNRS) *) module CoincidenceCount use import list.List use import set.Fset use import list.Elements use list.Mem as L use import int.Int clone export list.Sorted with type t = int, predicate le = (<), goal Transitive.Trans let rec coincidence_count (a b: list int) : set int requires { sorted a } requires { sorted b } ensures { result == inter (elements a) (elements b) } `````` Jean-Christophe Filliâtre committed Mar 29, 2016 31 `````` variant { a, b } `````` Jean-Christophe Filliâtre committed Mar 29, 2016 32 33 34 35 36 37 38 39 40 41 42 43 44 45 `````` = match a, b with | Cons ha ta, Cons hb tb -> if ha = hb then add ha (coincidence_count ta tb) else if ha < hb then coincidence_count ta b else coincidence_count a tb | _ -> empty end end `````` Jean-Christophe Filliâtre committed Mar 29, 2016 46 47 48 49 50 51 52 53 54 55 56 `````` (* the same, with elements of any type *) module CoincidenceCountAnyType use import list.List use import set.Fset use import list.Elements use list.Mem as L use import int.Int `````` Guillaume Melquiond committed Jun 16, 2016 57 58 59 60 61 62 `````` type t val predicate eq (x y : t) ensures { result <-> x = y } val predicate rel (x y : t) `````` Andrei Paskevich committed Jun 14, 2018 63 `````` clone import relations.TotalStrictOrder with type t, predicate rel, axiom . `````` Jean-Christophe Filliâtre committed Mar 29, 2016 64 65 66 67 68 69 70 71 72 73 74 75 `````` clone export list.Sorted with type t = t, predicate le = rel, goal Transitive.Trans let rec coincidence_count (a b: list t) : set t requires { sorted a } requires { sorted b } ensures { result == inter (elements a) (elements b) } variant { a, b } = match a, b with | Cons ha ta, Cons hb tb -> `````` Guillaume Melquiond committed Jun 16, 2016 76 `````` if eq ha hb then `````` Jean-Christophe Filliâtre committed Mar 29, 2016 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 `````` add ha (coincidence_count ta tb) else if rel ha hb then coincidence_count ta b else coincidence_count a tb | _ -> empty end end (* the same, using only lists *) module CoincidenceCountList use import list.List use import list.Mem use import int.Int clone export list.Sorted with type t = int, predicate le = (<), goal Transitive.Trans let rec coincidence_count (a b: list int) : list int requires { sorted a } requires { sorted b } ensures { forall x. mem x result <-> mem x a /\ mem x b } variant { a, b } = match a, b with | Cons ha ta, Cons hb tb -> if ha = hb then Cons ha (coincidence_count ta tb) else if ha < hb then coincidence_count ta b else coincidence_count a tb | _ -> Nil end end``````