Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

counting_sort.mlw 4.34 KB
 Jean-Christophe Filliâtre committed Feb 07, 2012 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 `````` (* Counting Sort. We sort an array of integers, assuming all elements are in the range 0..k-1 We simply count the elements equal to x, for each x in 0..k-1, and then (re)fill the array with two nested loops. TODO: Implement and prove a *stable* variant of counting sort, as proposed in Introduction to Algorithms Cormen, Leiserson, Rivest The MIT Press (2nd edition) Section 9.2, page 175 *) module Spec `````` Guillaume Melquiond committed Aug 21, 2014 20 `````` use export int.Int `````` Jean-Christophe Filliâtre committed Nov 23, 2014 21 `````` use int.NumOf as N `````` Andrei Paskevich committed Oct 13, 2012 22 `````` use export array.Array `````` Jean-Christophe Filliâtre committed Mar 28, 2014 23 `````` use export array.IntArraySorted `````` Jean-Christophe Filliâtre committed Feb 07, 2012 24 25 `````` (* values of the array are in the range 0..k-1 *) `````` MARCHE Claude committed Jan 28, 2014 26 `````` constant k: int `````` Jean-Christophe Filliâtre committed Feb 07, 2012 27 28 29 30 31 32 33 34 `````` axiom k_positive: 0 < k predicate k_values (a: array int) = forall i: int. 0 <= i < length a -> 0 <= a[i] < k (* we introduce two predicates: - [numeq a v l u] is the number of values in a[l..u[ equal to v - [numlt a v l u] is the number of values in a[l..u[ less than v *) `````` Jean-Christophe Filliâtre committed Nov 23, 2014 35 36 `````` function numeq (a: array int) (v i j : int) : int = N.numof (\ k. a[k] = v) i j `````` Jean-Christophe Filliâtre committed Feb 07, 2012 37 `````` `````` Jean-Christophe Filliâtre committed Nov 23, 2014 38 39 `````` function numlt (a: array int) (v i j : int) : int = N.numof (\ k. a[k] < v) i j `````` Jean-Christophe Filliâtre committed Feb 07, 2012 40 41 `````` (* an ovious lemma relates numeq and numlt *) `````` Jean-Christophe Filliâtre committed Nov 23, 2014 42 43 44 45 46 47 48 `````` let rec lemma eqlt (a: array int) (v: int) (l u: int) requires { k_values a } requires { 0 <= v < k } requires { 0 <= l < u <= length a } ensures { numlt a v l u + numeq a v l u = numlt a (v+1) l u } variant { u - l } = if l < u-1 then eqlt a v (l+1) u `````` Jean-Christophe Filliâtre committed Feb 07, 2012 49 50 51 52 53 54 55 56 57 58 59 `````` (* permutation of two arrays is here conveniently defined using [numeq] i.e. as the equality of the two multi-sets *) predicate permut (a b: array int) = length a = length b /\ forall v: int. 0 <= v < k -> numeq a v 0 (length a) = numeq b v 0 (length b) end module CountingSort `````` Andrei Paskevich committed Oct 13, 2012 60 61 `````` use import Spec use import ref.Refint `````` Jean-Christophe Filliâtre committed Feb 07, 2012 62 63 `````` (* sorts array a into array b *) `````` Andrei Paskevich committed Oct 13, 2012 64 `````` let counting_sort (a: array int) (b: array int) `````` Andrei Paskevich committed Jan 30, 2013 65 `````` requires { k_values a /\ length a = length b } `````` Andrei Paskevich committed Oct 13, 2012 66 67 `````` ensures { sorted b /\ permut a b } = let c = make k 0 in `````` Jean-Christophe Filliâtre committed Feb 07, 2012 68 69 70 71 72 73 74 `````` for i = 0 to length a - 1 do invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i } let v = a[i] in c[v] <- c[v] + 1 done; let j = ref 0 in for v = 0 to k-1 do `````` Andrei Paskevich committed Oct 13, 2012 75 76 77 78 79 `````` invariant { !j = numlt a v 0 (length a) } invariant { sorted_sub b 0 !j } invariant { forall e: int. 0 <= e < !j -> 0 <= b[e] < v } invariant { forall f: int. 0 <= f < v -> numeq b f 0 !j = numeq a f 0 (length a) } `````` Jean-Christophe Filliâtre committed Feb 07, 2012 80 `````` for i = 1 to c[v] do `````` Andrei Paskevich committed Oct 13, 2012 81 82 83 84 85 86 `````` invariant { !j -i+1 = numlt a v 0 (length a) } invariant { sorted_sub b 0 !j } invariant { forall e: int. 0 <= e < !j -> 0 <= b[e] <= v } invariant { forall f: int. 0 <= f < v -> numeq b f 0 !j = numeq a f 0 (length a) } invariant { numeq b v 0 !j = i-1 } `````` Jean-Christophe Filliâtre committed Feb 07, 2012 87 88 89 90 91 92 93 94 95 96 `````` b[!j] <- v; incr j done done; assert { !j = length b } end module InPlaceCountingSort `````` Andrei Paskevich committed Oct 13, 2012 97 98 `````` use import Spec use import ref.Refint `````` Jean-Christophe Filliâtre committed Feb 07, 2012 99 100 `````` (* sorts array a in place *) `````` Andrei Paskevich committed Oct 13, 2012 101 `````` let in_place_counting_sort (a: array int) `````` Andrei Paskevich committed Jan 30, 2013 102 `````` requires { k_values a } `````` Andrei Paskevich committed Oct 13, 2012 103 104 `````` ensures { sorted a /\ permut (old a) a } = 'L: `````` Jean-Christophe Filliâtre committed Feb 07, 2012 105 106 107 108 109 110 111 112 `````` let c = make k 0 in for i = 0 to length a - 1 do invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i } let v = a[i] in c[v] <- c[v] + 1 done; let j = ref 0 in for v = 0 to k-1 do `````` Andrei Paskevich committed Oct 13, 2012 113 114 115 116 117 `````` invariant { !j = numlt (at a 'L) v 0 (length a) } invariant { sorted_sub a 0 !j } invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] < v } invariant { forall f: int. 0 <= f < v -> numeq a f 0 !j = numeq (at a 'L) f 0 (length a) } `````` Jean-Christophe Filliâtre committed Feb 07, 2012 118 `````` for i = 1 to c[v] do `````` Andrei Paskevich committed Oct 13, 2012 119 120 121 122 123 124 `````` invariant { !j -i+1 = numlt (at a 'L) v 0 (length a) } invariant { sorted_sub a 0 !j } invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] <= v } invariant { forall f: int. 0 <= f < v -> numeq a f 0 !j = numeq (at a 'L) f 0 (length a) } invariant { numeq a v 0 !j = i-1 } `````` Jean-Christophe Filliâtre committed Feb 07, 2012 125 `````` a[!j] <- v; `````` Clément Fumex committed Jun 04, 2015 126 127 `````` incr j; assert {forall f. 0 <= f < v -> numeq a f 0 !j = numeq a f 0 (!j - 1)} `````` Jean-Christophe Filliâtre committed Feb 07, 2012 128 129 130 131 132 133 134 135 `````` done done; assert { !j = length a } end module Harness `````` Andrei Paskevich committed Oct 13, 2012 136 137 `````` use import Spec use import InPlaceCountingSort `````` Jean-Christophe Filliâtre committed Feb 07, 2012 138 `````` `````` Andrei Paskevich committed Oct 13, 2012 139 `````` let harness () requires { k = 2 } = `````` Jean-Christophe Filliâtre committed Feb 07, 2012 140 141 142 143 144 145 146 147 148 149 150 151 `````` (* a is [0;1;0] *) let a = make 3 0 in a[1] <- 1; in_place_counting_sort a; (* b is now [0;0;1] *) assert { numeq a 0 0 3 = 2 }; assert { numeq a 1 0 3 = 1 }; assert { a[0] = 0 }; assert { a[1] = 0 }; assert { a[2] = 1 } end``````