Report Number: CS-TR-80-779
Institution: Stanford University, Department of Computer Science
Title: Problematic features of programming languages: a situational-calculus approach
Author: Manna, Z ohar
Author: Waldinger, Richard J.
Date: September 1980
Abstract: Certain features of programming languages, such as data structure operations and procedure call mechanisms, have been found to resist formalization by classical techniques. An alternate approach is presented, based on a "situational calculus," which makes explicit reference to the states of a computation. For each state, a distinction is drawn between an expression, its value, and the location of the value. Within this conceptual framework, the features of a programming language can be described axiomatically. Programs in the language can then be synthesized, executed, verified, or transformed by performing deductions in this axiomatic system. Properties of entire classes of programs, and of programming languages, can also be expressed and proved in this way. The approach is amenable to machine implementation. In a situational-calculus formalism it is possible to model precisely many "problematic" features of programming langauges, including operations on such data structures as arrays, pointers, lists, and records, and such procedure call mechanisms as call-by-reference, call-by-value, and call-by-name. No particular obstacle is presented by aliasing between variables, by declarations, or by recursive procedures. The paper is divided into three parts, focusing respectively on the assignment statement, on data structure operations, and on procedure call mechanisms. In this first part, we introduce the conceptual framework to be applied throughout and present the axiomatic definition of the assignment statement. If suitable restrictions on the programming language are imposed, the well-known Hoare assignment axiom can then be proved as a theorem. However, our definition can also describe the assignment statement of unrestricted programming languages, for which the Hoare axiom does not hold.
http://i.stanford.edu/pub/cstr/reports/cs/tr/80/779/CS-TR-80-779.pdf