The multiple assignment statement
The conventional axiomatic definitions are given for multiple assignment to simple variables and for assignment to a single subscripted variable, along with examples to illustrate their use. The original contributions of this paper are the extension of the definition to include multiple assignment to several subscripted variables, and the development of a nontrivial, practical algorithm in which multiple assignment to several subscripted variables is indeed useful. Arguments are given to support the conjecture that the use of subscripted variables, like the use of pointers, can lead to exponential explosion of the length of a proof (and thus of the time needed to understand a program) unless the programmer is careful.
KeywordsArray Element Simple Variable Proof Rule Multiple Assignment Weak Precondition
Unable to display preview. Download preview PDF.
- E.W. Dijkstra, A Discipline of Programming. Englewood Cliffs, N.J.: Prentice-Hall, 1976.Google Scholar
- D. Gries, Assignment to subscripted variables, Computer Science Department, Cornell University, Tech. Rep. 77–305, Sept. 1976.Google Scholar
- C.A.R. Hoare, An axiomatic approach to computer programming, CACM 12 (Oct 69), 576–580, 583.Google Scholar
- C.A.R. Hoare and N. Wirth, An axiomatic definition of the programming language PASCAL, Acta Informatica 2 (1973), 335–355.Google Scholar
- D.E. Knuth, The Art of Computer Programming, vol. 3. Reading, MA: Addison-Wesley, 1973.Google Scholar