Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

Publication Details

Problematic Features Of Programming Languages: Situational-Calculus, Approach Part I: Assignment Statements

by Manna, Zohar and Waldinger, Richard

Technical Note 226
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave., Menlo Park, CA 94025
Nov 1980.

Order an AIC Technical Note

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 languages, 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.

Electronic Copies


Adobe PDF

BibTeX

EndNote

AIC Personnel

Name Title E-mail
Waldinger, Richard J Principal Scientist

SRI International
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy