Making variables abstract: an equational theory for Russell

ABSTRACT

One of the fundamental notions of programming, and thus of programming languages, is the variable. Recently, the variable has come under attack. The proponents of "functional programming" have argued that variables are at the root of all our problems in programming. They claim that we must rid our languages of all manifestations of the "vonNeumann bottleneck" and learn to live in the changeless world of functional combinators.While we may not, believe all the claims of the functional programming advocates, there is evidence that the treatment of variables in most programming languages leaves much to be desired. In this paper we discuss how to make variables "abstract", i.e., how to introduce the notion of variable in to a language so that variables have reasonable mathematical properties. This paper includes:--- a discussion of language design principles that allow a more mathematical treatment of variables in programming language, and--- a description of an equational logic for the programming language Russell [Boehm80]. Although this logic follows much of the development of abstract data types (cf. [Guttag78]), it is novel in its treatment of a language in which expressions not only produce values but also can have effects. We discuss the over all structure of the logic and present in detail the rules particularly relevant to the semantics of variables. A complete presentation of the logic appears in [Demers82], and the rule numbers in this paper agree with the numbers used there.In the next section, we discuss the underlying language principles needed to make an equational specification of variables possible. In the sections that follow, we present a logic that does so for Russell.

REFERENCES

• 1: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 2: {Bates82} Bates, J. and R. Constable. The definition of µprl. TR-82-492, Department of Computer Science, Cornell University, 1982.
• 3: Hans Boehm , Alan J. Demers , James E. Donahue, An Informal Description of Russell, Cornell University, Ithaca, NY, 1980
• 4: Hans-J. Boehm, A logic for expressions with side-effects, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582182]
• 5: Robert Cartwright , Derek Oppen, Unrestricted procedure calls in Hoare's logic, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.131-140, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512774]
• 6: J. W. de Bakker, Mathematical Theory of Program Correctness, Prentice-Hall, Inc., Upper Saddle River, NJ, 1980
• 7: Alan Demers , James Donahue, "Type-completeness" as a language principle, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-244, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567469]
• 8: {Demers82} Demers, A. and J. Donahue. An equational theory for Russell. TR-82-534, Department of Computer Science, Cornell University, 1982.
• 9: {Dijkstra72} Dijkstra, E. Notes on structured programming. In Dahl, O-J., E. W. Dijkstra and C. A. R. Hoare, Structured Programming, Academic Press, 1972.
• 10: {Guttag78} Guttag, J. and J. Horning. The algebraic specification of data types. Acta Informatica 10 (1978), pp. 27-52.
• 11: {Hoare72} Hoare, C. A. R. Proofs of correctness of data representations. Acta Informatica 1 (1972), pp. 271-281.
• 12: P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
• 13: {Martin-Lof79} Constructive mathematics and computer programming. Sixth International Congress for Logic, Methodology and Philosophy of Science, Hanover, Germany (1979).
• 14: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]