PROGRAMS WITH ARRAYS

{Pre} a(i) := expresision; {Post}

In order to deal with indexed variable, the
backward substitution rule must be generalized.

Post condition: Post
Statement: a(i) := expression

The Pre condition is obtained by substituting
every occurrence of an indexed variable a(i)
by the term:

if j=i then expression else a(j);