coincidence_count_list.mlw 2.6 KB
 Jean-Christophe Filliatre 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 Filliatre committed Mar 29, 2016 11 `````` See also coincidence_count.mlw for a version using arrays. `````` Jean-Christophe Filliatre committed Mar 29, 2016 12 13 14 15 16 17 `````` Authors: Jean-Christophe Filliâtre (CNRS) *) module CoincidenceCount `````` Andrei Paskevich committed Jun 15, 2018 18 `````` use list.List `````` Jean-Christophe Filliatre committed Mar 07, 2019 19 `````` use set.SetAppInt `````` Andrei Paskevich committed Jun 15, 2018 20 `````` use list.Elements `````` Jean-Christophe Filliatre committed Mar 29, 2016 21 `````` use list.Mem as L `````` Andrei Paskevich committed Jun 15, 2018 22 `````` use int.Int `````` Jean-Christophe Filliatre committed Mar 29, 2016 23 24 25 26 `````` clone export list.Sorted with type t = int, predicate le = (<), goal Transitive.Trans `````` Jean-Christophe Filliatre committed Mar 07, 2019 27 `````` let rec coincidence_count (a b: list int) : set `````` Jean-Christophe Filliatre committed Mar 29, 2016 28 29 30 `````` requires { sorted a } requires { sorted b } ensures { result == inter (elements a) (elements b) } `````` Jean-Christophe Filliatre committed Mar 29, 2016 31 `````` variant { a, b } `````` Jean-Christophe Filliatre committed Mar 29, 2016 32 33 34 35 36 37 38 39 40 41 `````` = 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 | _ -> `````` Jean-Christophe Filliatre committed Mar 07, 2019 42 `````` empty () `````` Jean-Christophe Filliatre committed Mar 29, 2016 43 44 45 `````` end end `````` Jean-Christophe Filliatre committed Mar 29, 2016 46 47 48 49 50 `````` (* the same, with elements of any type *) module CoincidenceCountAnyType `````` Andrei Paskevich committed Jun 15, 2018 51 52 `````` use list.List use list.Elements `````` Jean-Christophe Filliatre committed Mar 29, 2016 53 `````` use list.Mem as L `````` Andrei Paskevich committed Jun 15, 2018 54 `````` use int.Int `````` Jean-Christophe Filliatre committed Mar 29, 2016 55 `````` `````` Guillaume Melquiond committed Jun 16, 2016 56 57 58 59 `````` type t val predicate eq (x y : t) ensures { result <-> x = y } `````` Jean-Christophe Filliatre committed Mar 07, 2019 60 61 62 `````` clone set.SetApp with type elt = t, val eq = eq `````` Guillaume Melquiond committed Jun 16, 2016 63 64 `````` val predicate rel (x y : t) `````` Andrei Paskevich committed Jun 15, 2018 65 `````` clone relations.TotalStrictOrder with type t, predicate rel, axiom . `````` Jean-Christophe Filliatre committed Mar 29, 2016 66 67 68 69 `````` clone export list.Sorted with type t = t, predicate le = rel, goal Transitive.Trans `````` Jean-Christophe Filliatre committed Mar 07, 2019 70 `````` let rec coincidence_count (a b: list t) : set `````` Jean-Christophe Filliatre committed Mar 29, 2016 71 72 73 74 75 76 77 `````` 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 78 `````` if eq ha hb then `````` Jean-Christophe Filliatre committed Mar 29, 2016 79 80 81 82 83 84 `````` add ha (coincidence_count ta tb) else if rel ha hb then coincidence_count ta b else coincidence_count a tb | _ -> `````` Jean-Christophe Filliatre committed Mar 07, 2019 85 `````` empty () `````` Jean-Christophe Filliatre committed Mar 29, 2016 86 87 88 89 90 91 92 93 `````` end end (* the same, using only lists *) module CoincidenceCountList `````` Andrei Paskevich committed Jun 15, 2018 94 95 96 `````` use list.List use list.Mem use int.Int `````` Jean-Christophe Filliatre committed Mar 29, 2016 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 `````` 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``````