|
 ABSTRACT
A variety of concepts, laws, and notations are presented which facilitate reasoning about arrays. The basic concepts include intervals and their partitions, functional restriction, images, pointwise extension of relations, ordering, single-point variation of functions, various equivalence relations for array values, and concatenation. The effectiveness of these ideas is illustrated by informal descriptions of algorithms for binary search and merging, and by a short formal proof.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
Burstall, R.M. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7 (Nov. 1972), 23-49.
|
| |
2
|
Cooper, D.C. Proofs about programs with one-dimensional arrays. Unpublished.
|
| |
3
|
|
| |
4
|
Floyd, R.W. Assigning meanings to programs. Proc. Symp. in Applied Mathematics, Vol. 19, Amer. Math. Soc., Providence, R.I., 1967, pp. 19-32.
|
 |
5
|
|
| |
6
|
|
| |
7
|
Hoare, C.A.R. Notes on data structuring. In Structured Programming, O.-J. Dahl, E.W. Dijkstra, and C.A.R. Hoare, Academic Press, N.Y., 1972, pp. 83-174.
|
| |
8
|
Hoare, C.A.R. A note on the FOR statement. BIT 12, 3 (1972), 334-341.
|
| |
9
|
Hoare, C.A.R., and Wirth, N. An axiomatic definition of the programming language PASCAL. Acta lnformatica 2 (1973), 335- 355.
|
| |
10
|
McCarthy, J., and Painter, J. Correctness of a compiler for arithmetic expressions. Proc. Symp. in Applied Mathematics, Vol. 19, Amer. Math. Soc., Providence, R.I., 1967, pp. 33-41.
|
| |
11
|
Reynolds, J.C. Programming with transition diagrams. In Programming Methodology, A Collection of Papers by Members of IFIP WG 2.3, D. Gries, Ed., Springer-Verlag, 1978, pp. 153-165.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf