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]) }