The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Assignment and Procedure Call Proof Rules
The work
| Authors | David Gries; Gary Levin |
|---|---|
| Editors | |
| Type | article |
| Year | 1980 |
| Citekey | gries1980assignment |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery (ACM) |
| Volume | 2 |
| Issue | 4 |
| Pages | 564--579 |
Identifiers
| DOI | 10.1145/357114.357119 |
|---|---|
| ISSN | 0164-0925 |
Access
| Landing page | https://doi.org/10.1145/357114.357119 |
|---|
From crossref.
Abstract
The multiple assignment statement is defined in full generality—including assignment to subscripted variables and record fields—using the “axiomatic” approach of Hoare. Proof rules are developed for calls of procedures using global variables, var parameters, result parameters, and value parameters, using the idea of multiple assignment to provide understanding. An attempt is made to clarify some issues that have arisen concerning the use of rules of inference to aid in generating “verification conditions” in mechanical verifiers and the use of logical variables to denote initial values of program variables.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-24 07:54 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{gries1980assignment,
title = {Assignment and Procedure Call Proof Rules},
author = {David Gries and Gary Levin},
year = {1980},
journal = {ACM Transactions on Programming Languages and Systems},
publisher = {Association for Computing Machinery (ACM)},
volume = {2},
number = {4},
pages = {564--579},
issn = {0164-0925},
doi = {10.1145/357114.357119},
}
This record lives at https://refs.drheap.org/gries1980assignment/ and will keep doing so.