Sorting

Program sort1
  assign
    ([] i: 0 <=i<N ::
      A[i], A[i+1] := A[i+1], A[i] if A[i] > A[i+1])
end {sort1}

Program sort2
  assign
    (|| i: 0 <=i<N and even(i) ::
      A[i], A[i+1] := A[i+1], A[i] if A[i] > A[i+1])
  [] (|| i: 0 <=i<N and odd(i) ::
      A[i], A[i+1] := A[i+1], A[i] if A[i] > A[i+1])
end {sort2}

Program sort3
  assign
  [] ([] j: 0 <=j<=1 ::
    (|| i: 0 <=i<N and j = i mod 2 ::
      A[i], A[i+1] := A[i+1], A[i] if A[i] > A[i+1]))
end {sort3}