include "arrays.why" axiom mean : forall l,u:int. l < u -> l <= (l+u)/2 < u parameter merge : a:int array -> l:int -> m:int -> u:int -> { l <= m < u and sorted_array(a,l,m) and sorted_array(a,m+1,u) } unit writes a { sorted_array(a, l, u) and permut(a@, a, l, u) } let rec mergesort (a:int array) (l:int) (u:int) : unit = { } init: if l < u then begin let m = (l+u)/2 in mergesort a l m; assert {permut(a@init, a, l, u) }; mergesort a (m+1) u; merge a l m u end { sorted_array(a, l, u) and permut(a@, a, l, u) } (* Local Variables: compile-command: "gwhy mergesort.why" End: *)