#include "arrays.pi"

define int ix = ?;

@pre  true
@post forall(ix, 0, length(rv) - 1, rv[ix] >= 0)
int[] abs(int[] a)
declare
  int i;
{
  for
    @ true
    (i = 0; i < length(a); i = i + 1) 
  {
    if (a[i] < 0) {
      a[i] = -a[i];
    }
  }
  return a;
}