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 into a language so that variables have reasonable mathematical properties.

This paper includes:

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.

In designing Russell, we gave considerable thought to Backus's criticisms of "vonNeumann" languages [Backus78]. We were (and remain) convinced that any general-purpose programming language must incorporate some notion of variable and state. However, we were concerned that

We feel that we have achieved both of these goals. Below we present the equational theory of Russell. It is small enough to fit on a few pages of text, yet we feel it provides the essential insights a programmer needs.

The development of an equational logic for Russell was significantly aided by two important design decisions. The first of these was to adopt the principle of type-completeness [Demers80]. Basically, type-completeness means

Because Russell is type-complete, it has a simple, clearly identifiable language core of combining forms and then a larger set of interchangeable parts. These interchangeable parts include the builtin types and, most importantly for our purposes, the operations on variables. In most programming languages variables can be manipulated by programs (they can be passed as arguments to procedures, for example) but the operations that manipulate them are not all part of the surface syntax of the language. Assignment usually is a named primitive operation, but other operations like variable allocation usually are not, making it impossible to define the semantics of variables using the same logic that defines the non-variable component of the language.

There are compelling reasons for this -- few languages have type structures rich enough to describe such operations as variable allocation. Type-completeness makes it possible for all the operations that manipulate variables in Russell to be named functions in the programming language. Making Russell type-complete allowed us to bring the operations on variables up to the surface, so that the same equational theory that defines the language core can also define the parts of the language that manipulate variables.

The other important design decision was to begin developing an equational proof system for Russell before the language design was frozen. While developing the equational system, we found places where critical properties of the operations on variables could not be expressed as equations among expressions of the language. Our decision to develop an equational specification had an interesting consequence -- instead of enriching an assertion language for describing Russell, we were forced to enrich the programming language itself. It seems to us that this is an important point. A good deal has been written about the need to develop a language and its proof rules simultaneously; the hope is that the language will be molded by the desire to keep its proof rules simple. The use of an equational system puts an interesting twist on this idea: the requirements of the proof rules may point out areas where the programming language should be made more expressive.

In the following section we describe the Russell language subset used in this paper. We then present the overall structure of our equational proof system, and discuss the most important inference rules. The complete set of rules is given in [Demers82]. Next we discuss proof rules for operations on simple variables. We give two sample proofs to convey the flavor of reasoning in the system. Finally, we give rules for composite variables (records) which show how their semantics are straightforward compositions of the semantics of their components.

The language used below is a minor modification of Russell [Boehm80]. As we have already remarked, Russell is a type-complete language. It includes function- and type-valued expressions and treats them on an equal footing with more conventional expressions.

Russell is statically typed. As described below, the Russell logic includes rules by which we associate with each expression e a syntactic type specifier or signature S. The signature of e tells whether e denotes a value or a variable, and gives an expression for the type of e. Thus, a signature has the form "var exp" or "val exp" where, informally, "exp" must be a type-valued Russell expression. Formally, S is a legal signature iff the formula legal S is provable in the logic.

Expressions have a fairly conventional syntax. In the following description, variables beginning with p,q,...,x,y,z represent identifiers; variables beginning with d,...,h or T represent expressions; and those beginning with S represent signatures. A Russell expression may be any of:

The first task in specifying the semantics of variables is to find a set of operations suitable for characterizing their behavior. What sort of behavior must be captured?

In Russell the operations of assignment and value extraction, the predicates that test for aliasing and the operation of allocating a new variable are all just particular builtin functions. Thus it seemed natural to apply the ideas of abstract data type specification, where semantics is given by a set of equations relating the results of function applications, to defining Russell. In doing so we encountered two problems not common to the usual equational specifications:

Russell expressions can have effects, as well as produce values -- that is the whole point of having variables in the language. Thus, the equations of our system must relate not only the values of expressions but also the effects of evaluating them. In a sense, one of the major problems in the development of an equational theory for Russell is the semantics of the ";" operator.

Equivalences between expressions may hold only in certain contexts. For example, the following equivalence is obviously valid:

These constraints led us to a Gentzen-style deductive system having much in common with those of [Bates82] and [Martin-Lof79]. In the remainder of this section we present the basic structure of the system. In later sections we give the rules of inference that define our Russell subset.

The system includes some logical rules stating obvious basic facts about equivalences and typings. Among them are assumption and modus ponens rules, rules stating reflexivity, transitivity and symmetry of {, and substitution rules that allow provably equivalent expression to be substituted for one another in equivalence formulas and typings. These rules are straightforward, and can be found in [Demers82].

The Russell subset we are using includes builtin types int and bool with the Boolean, arithmetic and comparison operators +, -, *, /, d, ', (, etc. These operations treat values rather than variables, and in a Hoare-style system there are equivalent, identically-named functions in the assertion language. To enable us to reason about terms that use these operators, we include all rules of the form

Using the complete set of rules from [Demers82], we can show that if e1 and e2 use only the bool operators listed above, and if

In giving the semantics of a language in which expressions may have effects, it is necessary at times to limit the use of inference rules to only those subexpressions that are provably independent of state. For example, an equivalence such as

Purity is not the same as freedom from side-effects. Consider the expression "ValOf [ x ]", which extracts the value possessed by variable x. This expression has no effect, but its value manifestly depends on the state; thus it is not pure.

Conversely, evaluation of a pure expression can have an effect, since it does not necessarily terminate without error. Thus the plausible null effect rule

Since a pure expression is independent of the state, its effect must be the same -- abortion, nontermination, or no effect -- every time it is evaluated. Similarly, the value of a pure expression, if it has a value, must be the same every time it is evaluated. In short, a pure expression may be evaluated any number of times, provided it is evaluated at least once. The two rules

Earlier we described the rules by which we may deduce that a composite expression is pure. We shall also require signature rules for composite expressions, which allow us to deduce that expression e is type-correct by proving a formula of the form e: S. Finally, we shall require rules allowing us to deduce equivalences between composite expressions. The most important of the composite expression rules are discussed below; the remaining ones can be found in [Demers82].

The simplest signature rule is the one for sequential composition:

The signature rule for function applications is as follows:

The subgoals and conclusion of this rule involve simultaneous substitution of the argument expressions ei for the corresponding parameter names xi. These substitutions enable the rule to deal with type-valued parameters. For example, let p be the polymorphic identity function

The signature rule for let-blocks can be developed from the application signature rule. Following Landin's "principle of correspondence" [Landin66], we expect the expression

The remaining composite expression rules are those that allow us to deduce equivalences. A few of these rules are described below; a complete list appears in the [Demers82]. The most interesting and, for our purposes, the most important of the rules are the ones dealing with let-blocks, function applications and conditionals.

Most of the let rules are used to rename bound identifiers, to rearrange the components of a let-block, or to combine a block with an adjacent expression. For example, the rule

The following two rules allow let-blocks to be introduced and eliminated.

The most complex of the let rules is the following substitution rule:

Informally, gi { hi can be used as a predicate describing the bound values; so the general form of the rule allows us to use knowledge of the bound values in proving the equivalence of e and e'. For example, letting g1 be x1 and h1 be d1, we can derive the following extremely useful rule:

Two important rules give the meaning of function application:

Another important class of rules define conditional expressions. These include a signature rule, absorption rules analogous to the let absorption rules above, and a condition evaluation rule similar to application argument evalutation.

There are also three if elimination rules:

The most complex of the if rules is:

In Russell, the operations that manipulate variables are generally components of data types. Each builtin type T includes the components:

Note that the above rules leave many things unsaid about variables in Russell. They do not specify an implementation, but only the observable characteristics of variables in programs. Variable allocation may be done using a stack or a heap; the definition of New is insensitive to such implementation decisions. The operations of assignment or value extraction could have "benevolent side-effects" [Hoare72] like garbage collection; the only obligation is that after an assignment the only variable to yield a new value is the one to which the assignment was made.

To demonstrate the use of our equational system, we give two substantial examples.

The set of operations used above for simple variables forms the basis of the characterization of composite variables like records or arrays. Below we present the definition of records in Russell; arrays can be treated by a similar approach.

A Russell expression for a record type has the form

For this section, we let

To specify the meaning of the record type constructor, we must give meanings for each of the above operations. These meanings are defined in terms of the operations for the types Ti. In the rules that follow, we use the notation Ti$:=, Ti$ValOf and Ti$New for the assignment, value extraction and allocation functions for variables of type Ti.

Construction and field selection for record values are described by two simple rules:

The next few rules describe the aliasing behavior of the fields of record variables.

Finally, there are purity and null effect rules for the val and var field selector functions. The var rules

As an extended example, we illustrate that the obviously sound rule

In this paper we have presented an equational theory for Russell and argued that

The equational logic presented here is certainly not a complete replacement for a conventional Hoare-style system. Most importantly, there are no induction principles to allow proofs of general properties of program correctness. Theorems in this system can give the final results of program execution for particular inputs; but statements such as "for any integer n, this program computeds n!" are outside its scope. On the other hand, the fact that it is always possible to deduce the result of a terminating computation in the system argues that it gives a complete specification of variables; and this form of specification is a particularly pithy way to get across important properties of the programming language to potential users. In particular, there are components of the Russell equational theory that present the language better than any of our attempts at informal description. When writing the informal description of Russell and explaining the language to others, we often found that describing New as "allocating a new variable" was inadequate; moreover, the "operational" description of New conflicted with our desire to present a "mathematical" characterization of the language. It is far more edifying to give inference rules such as

In addition, as we noted above, the process of producing the equational theory led us to make some important changes in the language. It was only when we began to work on the theory that we found the need to introduce alias, contains and disjoint into the programming language. We now consider these operations to be perfectly natural and potentially quite useful.

[Backus78]

[Bates82]

[Boehm80]

[Boehm82]

[Cartwright78]

[deBakker80]

[Demers80]

[Demers82]

[Dijkstra72]

[Guttag78]

[Hoare72]

[Landin66]

[Martin-Lof79]

[McCarthy60]