Derived Semantics for Some Programming Language Constructs

1. Introduction

McCarthy and Painte r (8) proYe the correctness of a compiler for simple arithmetic expressions according to a definition of correctness first defined by McCarthy (7) . By means of an abstract anal)~ic syntax for the source language they give a functional description of its semantics. Similarly the semantics of an object language are specifiPd and then the rules governing a translation from the source language to the object language are defined. It is the correctness of this translator which is in question. The proof takes the form of shoving that the translated source phras e leaves the value predicted by the functional description of the source language semantics, in the accumulator of the object

machine.

There are strong parallels between the semantic description and the translation of a source language. Indeed, semantic description is accomplished by translation into a semantic object language \o'hich is usually of a functional nature, as opposed to the command structure of the machine language of an object machine. Conversely, the formal description of a translator, mapping the source language into such a procedural language is an adequate description of the source language semantics, given a description of the object language semantics. This point is made by ·.-irth (10).

In this paper we shall be concerned with an approach to implementation correctness veD' similar to McCarthy and Painter, except that we make no a priori description of the source language semantics and consequently no definition of correctness. Rather, we shall define a procedural object language and a translator mapping the source language into it. We shall derive from these definitions a functional description of the source language semantics. Correctness is then involved with the acceptance of this functional description as truly representing the meaning informally attributed to the source language. This is no less formal, except possibly in order of presentation, than the technique of McCarthy and Painter. Where those authors require acceptance of a definition of source language semantics a priori, this author requires the same a postiori.

The main results of this paper are taken from Henderson (3) where a programming language is presented, analysed and a functional description of its semantics derived. The techniques are presented there as a language design tool, since this is how they were developed. As such they are seWTely critical of irrational source language and implementation features. The language ALEPH, which is based on ideas from many current high level languages i s quite sophisticated, in that . it allows for recursively activated functions and has a block structure within the confines of which one may declare storage for arrays. Notably, however, ALEPH does not contain an explicit control transfer (goto) facility. It vas possible to derive a semantic description of the language up to but not including the use of vectors. The problem here vas that of "sharing" of storage which had been identified by Landin (6). In this paper, three of the morp interesting results will be described to illustrat e the techniques used. There is no doubt that thP constructs chosen are the simpl er ones deriYed in Henderson ( 3). It is hoped to publish other results, those concerning functions in particular, elsewhere.

2. Some programming language constructs

It is not npcessaD· to dPs cribe the \.'hole of a programming language in dPtail in order to discuss some of the constructs available in it. It i~ however, judicious to describe a little more than is formally necessaD· in order to cultivate understanding. Consider then a programming language in "hich a program is constructed from phrases called Pxpressions. Each expression is defined syntactically as a combination of symbols and phrases, some of which may be expressions. ~e shall not be concerned herP with phrases other than expressions. For reasons of expediency in semantic description vP do not distinguish the concPpt, familiarly knovn as a statement, in our language. Rather " e allow an expression to bP eYaluated solely for the side-effect it '-'ill have . This saves us , for example, having to define separate ly thP concept of conditional statement and conditional expression. In the casP of constructs more frequently asspciated vith a side-~ffect than a valu~ such as ass1gnment and 1terating statements, conventional and if possible, convenient values will be designated for them. An assignment statement may yield as its value, the value assigned, for example. This sort of concept is not new, it appears in Wirth (10) and others.

The three constructs we wish to consider can be defined as follows .

1. There are certain basic expressions, which we shall not specify, here, which perform primitive computations of a desirable nature. For example

)

then so is

2. If e ' e

• ). If e , e , e are expressions, then so
• 1 2 a if e 1 ~ e::> ~ e~
• If e and e are expressions, then so is 1 2 . .!!hi.!.! e do e 1- a

To define what each of these constructs means, it is necessary to consider what we mean by value aad side-effect. We assume that the computation expressed by a program manipulates the elements of some domain, which elements we shall call values. ~expression, therefore specifies the computation (assuming it terminates) of a value from this domain. We assume this computation takes place in an enviroa.ent consisting of a collection of variables, each of which may or may not possess a value. When an expression is evaluated it may or may not produce a value. When an expression is evaluated it may alter the values associated with some of these variables. This effect is known as the side-effect (of the eTaluation). In particular if the effect is to leave the variables unchanged, then it is said to be a null side-effect. A subset of the domain is~tinguished and called zero, wher~ssume it is possible to test ~lue for membership of this subset.

We shall see that this predicate is used to

construct conditional computations.

1. The value and side-effect of each basic expression is assumed to be defined.
2. The value and side-effect of evaluating

begin e ; e ; ···· ; e end 1 2 t -- is just the value and side-effect of evaluating e in the environment produced by evaluatin~ e , ··· , e in order from 1 t _l left to right.

2

... , e are expressions,

t

1. The value and side-effect of evaluating

is the value and side-effect of evaluating one of e or e in the environment produced :! :. by evaluating e· , according to whether the 1 value of e is in zero or not. 1 If the value of e is in~ then e is selected, l 3 otherwise e is selected.

:0

1. The side-effect of evaluating

is the side-effect of evaluating e and e 1 2 alternatelvd be~inning and ending with e 1 , unt1l 'tne v!Hue of e 1 , is first in ~· The value of

is the value produced by . e when it is last ::> evaluated according to the above scheme, or 0 (which is some element of zero) if e is - -- ::> not evaluated, that is when e yields an 1 element of ~ when first evaluated.

We shall not attempt to be more precise about this informal semantic description here. The nature of zero is confusing. To c larify, if the domain is the direct union of integers and booleans then zero may have the single element false. However, we do not wish to

confine these results to such a choice of domai~

), An implementation for a hrpothetical machine

Let us consider a computing device (not unlike a current day machine in which core and registers are used in a special way), which includes an accumulator T and a stack F. The names T and F were derived from the "top" element and the "first stacked" element in a single stack structure. The basic operations which this device can perform may be specified simply in terms of the accumulator T and the stack F as follows ,

• T·F place the current value ofT on top of the stack F, leave T unchanged .
• TlF replace the value of T by the value at the top of the stack. Remove this value from the stack.

~ F Remove the top value from the stack.

T~ replace the current value of T by Q.

The basic tests which the device can perform include:

(T~)? test if the current value of T i s in ~·

• A program for this device is a graph with a single entry and a single exit.

Th~ nodes of the graph are of three kinds.

1. Command: single entry, singlP exit,

labelled with a basi c operation.

single entry, double exit, labelled with a basic test and with the exits marked

1. Test: YES and NO.
2. Join:

double entry, single exit, unlabelled.

Such a program forms a flow diagram in a fairly obvious sense . We are now in a position to give the translations of our three principal expressions. Square brackets are used throughout merely to indicate structurP in a (meta) expression . Source expression s will be used autonomously.

Given an expression e in the source language, we denote by ue its translation to a program for our hypothetical computing device. In displaying this program as a graph we encircle the (unspecified) subgraphs for component expressions with a dotted line.

2. u~lf e ~ e l :e !..!.!! e 1

3. u[~ e do e J l 2

The as sumption, whi ch WP shall establish inducti\·ely in section 5 , in tha t the translat ­ ion of an expression is a program whi ch :

1. Stacks the current value ofT;
2. oth<> rwise 'leaves F unalter ed ;
3. ani ). leaves the valuP of thl' trans lat ed expression in T.

The program may of course have an effec t upon othPr, as yet unspecifi ed, component s of the device.

4. Notation for thP modPl

It is necessary to construct a model of our hypothetical computing deYice in ord e r to analyse thP programs which we heYe con5tructed for it. The notation is based on StracheY ( 1964) , Lend in ( 1963) and Curry and Fe~·s (1958) and other papPrs already c ited.

If f is a function end x an argument withi n the domain off, WP denot e by fx t hP r esult of applying f to this argument. Appli cation associates to the left, thus fx x · .. x

l ?. · "dot" product f.g, where f and g are function s over appropriat.e domains is defined by rf.g1x" frgx,. ThP function "dot " product ha s a lower binding power than appli cation and hence rfx.gy]z is interpreted as rfx~ rgyz" . Note that this product is associative and WP shall write 'f.g.hlx for frg r hx~~ ~ ·

By means of the notation of thP )-calculus we may write the definition of f.g a s f. g R >,xf(gxJ. J'ln a 1-expression the ). is followed immediately by the bound variable and then the body which extends as far to the right as is consistent with th.e bracketing. The )_-express­ ion, )x.A denotes the function, whose value for argument B, denoted by [ AxA)B, is obtained by evaluating the expression obtained when B is substituted f~r all free occurrences of x in A. We shell assume that B is evaluated before substitution and that anv clash of variables (if the result of B cont~ins any ). -expressions with free variables) is catered for by renaming of bound variables.

A particular function which we shall have need of is the following

Note that Cu\v selects v if u is in zero and w if it is not. In general a funct~f can be defined by a scheme

where· c is a combination of )-expressions and previously defined functi~ns. If , however , f contains an occurrence of f then we denote by

the sol u t i on of f = c, if it exists. Y is cal l ed th e paradoxical combinator by Curry and Feys ( 2) and the fixed-point operator by Landin (5). Eff ec t i ve ly it allows us to name the f un ction f ind ependently of the letter used to des i gnate it.

Finally, l et us introduce some notation for sta cks. f, denotes the empty stack and if S is t he s t a ck with the n elements S , S , ~

S we write

by s+ c n - lie denote the top element s and by s l t he sta ck remaining when s is removed.

'o'hen -.;e cons ide r the hypothetical computing devi ce, t her e are various elements whi ch can a l te r as the r esult of executing a command. Th~ a ccumul a to r and the stack can alt er, s ince al l t he ba s i c commands introduced here r ef er to t hem directly . The rest of the element s t hat can al te r ve shall call collectively t he ( source) en\·i ronment . The environment is effecth·e ly a data s tructu r e whi ch includes information about t he values of all currentlv declared variabl es. I f we denote the (source) ~nvironment by v we can conside r the object-environment F to be a t r i pl e

,.-her e t and f denot e the current value s of the accumulato r and the stack respectively. Th e not i on ( i s what McCarthy (7) refers t o a s a s tate vector. What we have done is simply to impart t o i t a lit t le mor~ structure .

The s eman t i cs of the object language can nov be de fin ed as mappings on the object-environment a s f oll o,.·s.

By compounding the effec t of these basi c obj ect-environment mappings we can derive t he ma ppi ng corresponding to a program for our hypotheti cal computing devi ce.

5 . Deriva t ion of s emanti cs for the three con s truc t s

The r ec ursive nature of the syntax g iven for t he expressi ons in section 2 necessita t es an induct i ve approach to derivat ionfur an expres si on. Gi ven an Pxpression e cons t ruc t ed from express ions e 1 , e 2 , elc we shall establish a lemma stating that e had a certain property under the assumption that e , e 2 ,

by an argument using structural induction, it is shown that for a certain choice of expresswn types, that such a lemma is sufficient to establish the property absolutely for e. The induction principle used is similar to that required by McCarthy and Painter and explained fully by Burstall ( 1 ).

The property which concerns us in this paper we shall call property A.

property A: the expres s ion e is said to possess property A, written A~ e,, if the result of evaluating e in the object-environment ' = rt,f,v] is the object-environment~ ~ = [t',(t,f),v'J whe re t' = gv and v ' = hv for some functions g and h, determined by the expression e.

We see that in particular the original value of t is saved and the new values of the accumulator and environment depend only on the old value of the environment. (~ote we mean source environment). The fun ction g is called the value function associated with e and h is the associated side- effect fun ct i on.

We shall assume that there exist functions C!' and ·I· such that given e, a s in the definition of property A, we have

Thus we can write

[t,f,v] ~ r~·ev, (t,f), 'i'ev1 since Are] to show the obJect-environment mapping due to an expression with property A. Note that ~~ and 1!1e are the functions whi ch determine the semantics of e. ~e are nov in a position to establish the lemmas whi ch we should use in an argument of correctness of the implementation of the three expressions introduced in section ~

~ If the expressions e , e , ··· , e l 2 lc possess property A then so does the expression

We shall prove by induction on the index k, that if

(t,f)' r l/ielc ..·.· '''e JvJ

l For if k = 1 we have I.L rbegin e l = I.L e and hence l end1

since Af' e ! . 1 .

which establishes our h~~othesis fork= 1.

The translation B for k > 1 , given in k section 3 can be written

-- - - - -- - - - - - - - - - -

which is

Hence

This compl etes the induction and shows that begin e 1 ; ··· ; ek end possesses property A with

lemma 2 If the expressions e 1 , e:<, and e 3 possess property A, then so does the expression

proof First we consider the derivation connected with the following diagram, for some e which has property A.

The diagram corresponds to the form of each arm of the conditional expression. The initial operation, T!F is used to remove the redundant value of the tested expression. This context allows us to assume that F is not empty .

Now in the program

the condition selects between two functions of the same form, thus

ft,f,v] ~ rct [we 3 ][tpe:<]v, f, Ct[ 41e)r'\'e)vJ for the value of the accumulator since this suggests that both e and e are evaluated.

2 3

Finally, for the whole program as shown in section 3 we have

which establishes property A, with:

lemma 3 If the expressions e and e possess l 2 property A, then so does the expression

while e do e l- 2

Consider the program:

we postulate that there exist functions o, B with the property that the object-environment mapping of this program (if it terminates) is Ve postulate that there exist functions ~ and ~ constructively by induction on k, the number of times the condition in the loop proves false.

Suppose k = 0, then the above program corresponds to

/ -,

which has

Thus the hypothesis is true for k 0, with

a-tv t

Suppose now the hypothesis is true in case we should go round the loop k- 1 times, and that in this case we have Cl'= a' and e p', then if the condition should prove false k times, we have the derivation.

by the inductive hypothesis, since condition proves false after k - 1 more loops. This establishes the hypothesis and ~ and p have the form

However, in for a and 8 derivations order to get a definitional form we must consider the partial chosen by the condition in the loop.

for the NO branch

Now for the whole diagr~, we have Now to establish property A, we have simply to construct a derivation for the whole program given in section 3.

which establishes property A. Ve have

r"[ while e do e 1 =

2

rna).t). vC(coe ~vt)().varcoe v]nhe vl}r,~e v]l 0

l

2

"" 2

''lrwhile e do e ] =

4 ---1-2

D.p>.vq coe v] [ >.vv) [ fl.l~e ] r,l,e v]

l

· I

l

5. Conclusions

In each of the above lemmas we have derived a value function and a side-effect function, for the expression concerned, in terms of the value and side-effect functions of the component expressions. These functions are in a form which this author has found convenient for manipulative purposes. The formulation would be called 'applicative' by Curry and Feys (2) (in a lose sense). They are not, 'however, in a digestible form for the definition of language in an educational sense. In Henderson (3), the result on the while expression is analysed and alternative forms given. In particular the side-effect function is shown to be equivalent to that defined by Hoare (4).

The requirement for formal semantic description, in the author's view, is most essential in the area of program correctness. Depending upon whether the correctness proof is the duty of the programmer or the machine, the semantic metalanguage must be so oriented. The meta language used here is only nominally oriented towards mechanical handling but this is an area in which the author is currently experimenting.

'I l

-

To summarise, we have defined a language informally and then an implementation for it. The semantics of the object language and the definition of a translator into the object language specify the semantics of the source language in a procedural way. By analysing the translation of the source phrase it has been possible to derive a functional · description of the source language semantics. Correctness of the implementation involves acceptance that the informal interpretation of the derived semanti c functions corresponds to the meaning informally attributed to the phrases when they were defined.

A final point worth noting is that the results presented here were developed in the context of a particular implementation. Yet they turned out to be remarkably independent of many of the design features of that implementation. This fact has enabled us to investigate just three of the constructs here without concern for the others. It is heartening to note that the demands of the proofs rationalised the language design to a point where it was easy to describe to both man and machine.

Acknowledgements

This research, which was carried out in the Computing Laboratory of the University of Newcastle upon Tyne from 1967 to 1970 , was supported initially by the Science ResParch Council and subsequently by the University . The author is extremely grateful to Mr. M.J. Elphick of the Laboratory for the time he devoted to reading and discussing this material.

• 1, Burstall, R.M, (1969) 'Proving properties of programs by structural induction'. Computer Journal. Vol 12, p. 41.
• Curry, H.F. and Feys, R. (1958) 'Combinatory Logic'. Vol. 1. North Holland, Amsterdam.
• Henderson, P. (1970) 'Design and Semantic Analysis of a programming language and its compiler'. Ph.D. Thesis, University of Newcastle upon Tyne.
• Hoare, C.R. (1969). 'An axiomatic basis for computer programming'. CACM, Vol. 12 Nov. 1969, p. 576.
• Landin, P.J. (1963) 'The mechanical evaluation of expressions', ComputPr Journal, Vol. 6, p. 308. 1963.
• Landin, P.J. (1965) 'A correspondence between Algol and Church's X-calculus'. CACM Vol. 8, 1965, p.89 + p.158.
• McCarthy, J. 'Towards a mathematical science of computation', IFIP Proc. (1962) p. 21.
• 8, McCarthy, J. and Painter, J. (1967) 'Correctness of a Compiler for Arithmetic
• expressions'. 1967 0 AMS Symp. in Appl. Math 19,
• Strachey, C. (1964) 'Towards a formal semantics~ in 'Formal language description languages for computer programming'. Ed. T.B. Steel. Publ. North Holland , 1964 IFIP Conf, Proc, Baden,
• Wirth, N. (1966) 'Euler, a generalisation of Algol and its formal definition' CACM , Vol. 9, p. 13.

Tvpographical note: In the iterated fumction "dot" product 1f1e · , · · · lhe the "do~ " should 1 k not be confused with the ellipses. A succession of three dots {s used consistently as ellipses, a single dot must therefore be interpreted as "dot" product.