program abs {
	declarations
		pre valid_index(t,i) && valid_index(t,j);
		post t[i] == old(t[j]) && t[j] == old(t[i]);
		subProgram swap(t -> Array[10], i -> Integer, j -> Integer) -> Array[10] {
			declarations
				tmp -> Integer;
			statements
				tmp := t[i];
				t[i] := t[j];
				t[j] := tmp;
				return t;
		};

	statements
		skip;
}
