muller.mlw 833 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 10 ``````module Muller use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 11 12 `````` use import ref.Refint use import 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 16 `````` function numof (a: array int) (l u: int) : int = N.numof (\ 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 Nov 23, 2014 21 `````` invariant { 0 <= !count = numof a 0 i <= 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 Nov 23, 2014 27 `````` invariant { 0 <= !count = numof a 0 i <= 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``````