include "arrays.why" (* exemple pour le Coq'Art *) logic l : int axiom l_pos : 0 < l parameter a : int array parameter x,y : int ref parameter swap : i:int -> j:int -> { array_length(a) = l} unit writes a { array_length(a) = l and a[i] = a@[j] and a[j] = a@[i] and forall k:int. 0 <= k < l -> k <> i -> k <> j -> a[k] = a@[k] } let pgm_max_end () = { array_length(a) = l } begin x := 0; y := 1; while !y < l do { invariant 0 <= y <= l and 0 <= x < l and (forall k:int. 0 <= k < y -> a[k] <= a[x]) variant l-y } if a[!y] > a[!x] then x := !y; y := !y + 1 done; (swap !x (l - 1)) end { (forall k:int. 0 <= k < l-1 -> k <> x -> a[k] = a@[k]) and a[x] = a@[l-1] and a[l-1] = a@[x] and (forall k:int. 0 <= k < l-1 -> a[k] <= a[l-1]) }