EXAMPLE OF PROGRAMS WITH ARRAYS

Insert an integer x into a table
of n elements.

{n < nmax}
if n < nmax then
n := n+1;
table(n) := x;
end if;
{n =< nmax and
(exists i (1=