include "arrays.why"

let swap =
  fun (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) }