include "arrays.why" (* maxisort: Maximum sort *) (* swapping two elements of an array *) let swap (t:int array)(i,j:int) = { 0 <= i < array_length(t) and 0 <= j < array_length(t) } (let v = t[i] in begin t[i] := t[j]; t[j] := v end) { exchange(t,t@,i,j) } (* Maximize(t,n,x,k) is forall i, k <= i <= n implies t[k]<= x *) (*external logic Maximize: int farray, int, int, int -> prop*) predicate Maximize(t:int array, n:int, x:int, k:int) = forall i:int. k <= i <= n -> t[k]<= x (* returns the index of the maximum element of t[0..n] *) let rec maximum (t:int array)(n,k,i:int): int { variant k } = { 0 <= k <= i and i <= n and n < array_length(t) and Maximize(t,n,t[i],k) } (if k=0 then i else let nk=k-1 in if t[nk]>t[i] then (maximum t n nk nk) else (maximum t n nk i)) { 0 <= result <= n and Maximize(t,n,t[result],0) } (* Maximum sort *) let maxisort (t:int array) = { 0 <= array_length(t) } init: (let i = ref ((array_length_ t)-1) in while !i >= 0 do { invariant 0 <= i+1 <= array_length(t) and sorted_array(t,i+1,array_length(t)-1) and permutation(t,t@init) and (i+1 < array_length(t) -> Maximize(t,i,t[i+1],0)) variant i+1 } (let r = (maximum t !i !i !i) in (swap t !i r)); i:=!i-1 done) { sorted_array(t,0,array_length(t)-1) and permutation(t,t@) }