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