The multiple assignment statement

  • David Gries
II. Program Verification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 69)


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.


Array Element Simple Variable Proof Rule Multiple Assignment Weak Precondition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    E.W. Dijkstra, A Discipline of Programming. Englewood Cliffs, N.J.: Prentice-Hall, 1976.Google Scholar
  2. [2]
    D. Gries, Assignment to subscripted variables, Computer Science Department, Cornell University, Tech. Rep. 77–305, Sept. 1976.Google Scholar
  3. [3]
    C.A.R. Hoare, An axiomatic approach to computer programming, CACM 12 (Oct 69), 576–580, 583.Google Scholar
  4. [4]
    C.A.R. Hoare and N. Wirth, An axiomatic definition of the programming language PASCAL, Acta Informatica 2 (1973), 335–355.Google Scholar
  5. [5]
    D.E. Knuth, The Art of Computer Programming, vol. 3. Reading, MA: Addison-Wesley, 1973.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1979

Authors and Affiliations

  • David Gries
    • 1
  1. 1.Cornell UniversityUSA

Personalised recommendations