muller.mlw 797 Bytes
 Jean-Christophe committed Apr 04, 2011 1 `````` `````` Jean-Christophe Filliatre committed Aug 18, 2011 2 3 4 5 6 7 ``````(* A small verification challenge proposed by Peter Müller. Given an array of integers, we first count how many non-zero values it contains. Then we allocate a new array with exactly this size and we fill it with the non-zero values. *) `````` Jean-Christophe committed Apr 04, 2011 8 9 ``````module Muller `````` Andrei Paskevich committed Jun 15, 2018 10 11 12 `````` use int.Int use ref.Refint use array.Array `````` Jean-Christophe Filliatre committed Nov 23, 2014 13 `````` use int.NumOf as N `````` Jean-Christophe committed Apr 04, 2011 14 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 15 `````` function numof (a: array int) (l u: int) : int = `````` Guillaume Melquiond committed Mar 16, 2016 16 `````` N.numof (fun i -> a[i] <> 0) l u `````` Jean-Christophe committed Apr 04, 2011 17 `````` `````` Jean-Christophe Filliatre committed Aug 18, 2011 18 `````` let compact (a: array int) = `````` Jean-Christophe committed Apr 04, 2011 19 `````` let count = ref 0 in `````` Jean-Christophe Filliatre committed May 17, 2011 20 `````` for i = 0 to length a - 1 do `````` Jean-Christophe Filliatre committed Jun 05, 2018 21 `````` invariant { !count = numof a 0 i } `````` Jean-Christophe committed Apr 04, 2011 22 23 24 25 26 `````` if a[i] <> 0 then incr count done; let u = make !count 0 in count := 0; for i = 0 to length a - 1 do `````` Jean-Christophe Filliatre committed Jun 05, 2018 27 `````` invariant { !count = numof a 0 i } `````` Jean-Christophe Filliatre committed May 17, 2011 28 `````` if a[i] <> 0 then begin u[!count] <- a[i]; incr count end `````` Jean-Christophe Filliatre committed May 16, 2011 29 `````` done `````` Jean-Christophe committed Apr 04, 2011 30 31 `````` end``````