Assignment to Subscripted Variables

Abstract

The assignment b(r):=e is investigated using two axiomatic definitions in order to gain an understanding of the problems involved with using arrays. It is seen that assignment to array elements leads to many of the difficulties encountered with pointers or references. The axiomatic definition is extended to cover the multiple assignment statement to both simple and subscripted variables, and a proof of correctness for a nontrivial program is outlined using the new definition.