Reasoning about arrays

Abstract

The use of complete and precise assertions, developed by Floyd and Hoare, is a powerful method for avoiding programming errors. For nontrivial programs, however, such assertions become extremely tedious when written in first-order predicate calculus.In the case of array-manipulating programs, this tedium can be alleviated by several notational and conceptual devices: (1) partition diagrams, which relate intervals of subscript values; (2) pointwise extension, which reduces the need for explicit quantification; and (3) a hierarchy of useful equivalence relations among array values.The effectiveness of these ideas is illustrated by programs for binary search and for merging. © 1980, ACM. All rights reserved.