Assigning meanings to programs
The work
| Authors | Robert W. Floyd |
|---|
| Editors | |
|---|
| Type | incollection |
|---|
| Year | 1993 |
|---|
| Citekey | floyd1993assigning |
|---|
Where it appeared
| Published in | Program Verification: Fundamental Issues in Computer Science |
|---|
| Publisher | Springer |
|---|
| Series | Studies in Cognitive Systems |
|---|
| Number in series | 14 |
|---|
| Pages | 65--81 |
|---|
Related
| Distinct from | colburn1993program |
|---|
| Distinct from | floyd1967assigning |
|---|
| Reprint of | floyd1967assigning The 1993 appearance in Colburn, Fetzer and Rankin's Program Verification: Fundamental Issues in Computer Science reprints the 1967 Proceedings of Symposia in Applied Mathematics paper. The pair was already linked distinct-from, which is true but says less than the relation warrants. |
|---|
Abstract
This paper attempts to provide an adequate basis for formal definitions of the meanings of programs in appropriately defined programming languages, in such a way that a rigorous standard is established for proofs about computer programs, including proofs of correctness, equivalence, and termination. The basis of our approach is the notion of an interpretation of a program: that is, an association of a proposition with each connection in the flow of control through a program, where the proposition is asserted to hold whenever that connection is taken. To prevent an interpretation from being chosen arbitrarily, a condition is imposed on each command of the program. This condition guarantees that whenever a command is reached by way of a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. Then by induction on the number of commands executed, one sees that if a program is entered by a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. By this means, we may prove certain properties of programs, particularly properties of the form: 'If the initial values of the program variables satisfy the relation R l, the final values on completion will satisfy the relation R 2'.