# Proof and synthesis of semantic attributes in compiler definition

Pierre Deransart

<figure><img src="image_1.png" /></figure>

## To cite this version:

Pierre Deransart. Proof and synthesis of semantic attributes in compiler definition. [Research Report] IRIA-RR-333, IRIA. 1978, pp.15. hal-04716529

HAL Id: hal-04716529

https://inria.hal.science/hal-04716529v1

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
RIA

laboria

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20

laboratoire de recherche
en informatique
et automatique

PROOF AND SYNTHESIS
OF SEMANTIC ATTRIBUTES
IN COMPILER DEFINITION

Pierre DERANSART

Rapport de Recherche N° 333

Décembre 1978

ASP.
PROOF AND SYNTHESIS OF SEMANTIC ATTRIBUTES IN COMPILER
DEFINITION

Pierre Deransart

Résumé :

La définition d'un compilateur par attributs sémantiques présente un inconvénient qui limite son
utilisation : elle comporte un grand nombre de définitions souvent triviales ainsi que des redon-
dances qui alourdissent la description et augmentent le risque d'erreurs d'écriture.

La description d'un compilateur par les seules définitions d'attributs guides et la synthèse des au-
tres définitions à partir de spécifications est présentée dans ce rapport comme un essai pour rédui-
re ces inconvénients. La synthèse est dérivée de la méthode de preuve introduite par Amirchahy,
Néel et Pair.

Abstract :

One of the drawbacks of compiler definition by semantic attributes is the great number of attri-
bute definitions and the redundancies that occure in such definitions. Automatic synthesis of
attribute definitions from some spécification plus driving attribute definition is presented as
an attempt to make such a method more practical. The synthesis is derived from the proof me-
thod as described by Amirchahy, Néel and Pair.

Mots clés : attributs sémantiques, compilateur, spécification de traducteur, synthèse d'attributs.

Key words : semantic attributes, compiler, translator writing system, compiler specification
attribute synthesis.
PROOF AND SYNTHESIS OF SEMANTIC ATTRIBUTES IN COMPILER DEFINITION

Pierre DERANSART

The purpose of this report is to present how proof and synthesis of semantic attributes definitions play complementary roles one to the other in facilitating the work of compilers writing (defined by semantic attributes) and in constructing partly correct compilers.

Semantic attributes were introduced by Knuth [Kn 68, 69, 71a, b] as a method for assigning meanings to derivation trees on context-free grammars. Such a system has been called a K-System, a declarative semantic [Fa 72, W 71, CM 77], an attributes grammar [Bo 76, JP 77], or a semantic attributes [Lo 74, Ne 75]. It is mostly used for compilers definition [Fa 72, Lo 75, Bor 75, Bo 72, GRW 77].

The synthesis of attributes definitions is motivated by a necessary large number of trivial definitions and numerous redondancies. Frequently for instance, an attribute condition is repeated in the different definitions of the same rule ; more frequently, in about 90% of the cases, definitions are reduced to identities. So it would be interesting to automatically generate a part of the definitions, using specifications characterised by relations between some attributes. In [De 78b] two methods of synthesis are presented, derived from a proof technique. Proof and synthesis are in fact complementary, because the problem of the synthesis is to find the missing definitions that permit to complete the proof.

The idea to use attribute grammars for proving purposes is relatively recent [Wi 75, NA 74]. Amirahay, Néel and Pair have presented in [ANP 78] a proof technique by attributes that uses an induction rule driven by the attributes dependencies. We propose here an improvement of this technique that decreases the possibilities of failure by extending the number of authorised hypothesis. This method uses the Lorbo-Pair algorithms [LP 75] to build the so called driving-attributes-network.

One of the aspects of this technique is to generalize the usual proof technique that generally corresponds to synthetised proof (proof driven by
synthetised attribute, i.e proofs working bottom-up wise in the derivation tree)
[Lon 71, CM 75]. It permits in fact to prove "synthetised" predicates as well
as "inherited" predicates and to transform a global proof - allways difficult -
into a set of proofs more limited but increasing the reliability of the
definition.

We show that it is possible to build a system that organizes the proof of
compiler specifications using the driving-attribute network, tries to synthetize
the missing definitions and otherwise tries the proof of the specifications.

Proof and synthesis can not be completely automatized. Even if it is
certainly difficult - or impossible - to automatically perform the complete
proof of a honest real compiler, we may try to prove automatically parts of
the compiler or, better, to write sufficient specifications that permit to
synthetize automatically the missing attributes definitions. If the synthesis
fails, we can write by hand the definitions and try to verify them by comple-
ting the proof.

In this report we illustrate such a method by an example of simplified
translation, with a symbol table, from Lisp-like functions into an object
language with three instructions on a stack of registers. To specify the
compiler it is necessary to introduce more attributes that needed by the
strict translation. Such supplementary attributes bring the necessary "elements
of comparison" to realize the proofs.

Section one describes how to improve the proof technique of [ANP 78] and
define driving attributes and driving-attribute network.

Section two presents the complete specifications of the simple compiler
by terms of an insufficient number of attributes definitions and a set of
assertions between attributes defined at the same non-terminal symbol of the
context-free grammar.

Section three introduces the synthesis of the definitions.

A certain knowledge about semantic attributes is assumed.

Section 1 : Proof technique, driving attributes network.

The objective of a *proof* by attributes is to prove some relations betwen
attributes of the same non-terminal symbol called assertion. The proof is
performed by induction. To perform a valid proof we have to consider some rule
of induction independent of any particular analysis. One solution is to
associate to each assertion one attribute (generally occurring in the
assertion) called **driving-attribute**. We denote by

$A_a^N$ an assertion valid at the non-terminal N and with driving-attribute
$a$. $a^N$ will denote the occurrence of some attribute a at the non-terminal N.

For each rule r of the grammar and for each attribute a defined in the rule r,
we define the set $B_{r,a}$ such that for any syntactical tree and for any order
of attributes evaluation we have.

$b \in B_{r,a} \Rightarrow b$ is evaluated before $a$.

Then, for each rule r, the scheme of the proof will be the following :

$$
\begin{array}{l}
\forall b \in B_{r,a} \quad A_b \wedge \text{Def}_{r} \vdots \quad A_a \quad (1) \\
\qquad \wedge \quad b \in B_{r,a}
\end{array}
$$

where $A_b$ is the conjunction of the assertions with driving-attribute b, and
$Def_r$ the conjunction of the definitions. The proof is valid under the assumption
of no cycle in attributes definitions (description coherency).

The problem is to determine $B_{r,a}$.

A first solution was proposed in [ANP 75, 78] with $B_{r,a} = \{b|b$ occurs
in the definition of a}. It appears generally sufficient, but in the example
(Appendix), if for $E_c^N$ we take s as driving attributs (Fig 3) - It is possible
because s and c progress together-then the proof of $E_s^{FO}$ in the rule 1 can not
be performed. It could be performed with the following second solution :

$B_{r,a} = \{b|a \text{ DS } b\}$. Where DS is a partial order relation under the
hypothesis of the description coherency, that intuitively corresponds to a
transitive closure of the direct dependencies between attributes, determined
by the definitions.

Let $G = (V_N, V_T, S_e, R)$ be a Context-free Grammar where $V_N$ is the
set of the non-terminal symbols, $V_T$ the set of the terminal symbols,
$S_e$ the axiom, $R$ the set of rewriting rules like : $X_0 \to \alpha_0 X_1 \alpha_1 X_2 \alpha_2 \dots X_n \alpha_n$
where $\alpha_i \in V_T^*$, $0 \le i \le n$ and $X_i \in V_N$, $0 \le i \le n$.

With each non-terminal N are associated two sets $I^N$ of **inherited** attributes and $S^N$ of **synthesized attributes** whose domains contain an undefined element. By definition an attribute is either inherited or synthesized and its value exists (eventually undefined) at all occurrences of the non-terminal where it is defined. In all the rules, the inherited attributes of the non-terminal symbols of the right part and the synthesized attributes of $X_0$ are computed. The **attributes definitions** are
expressed in a semantic definition language as functions of other
occurrences of attributes :

$$
a = f(b_1, b_2, \dots, b_p)
$$

where f is any function : $D_{b_1} \times D_{b_2} \times \dots D_{b_p} \to D_a$ (not taking into considera-
tion the constants occurring in the definition of f).

In a rule, a and b are related by a <u>direct dependency</u> from b to a
iff b occurs in the definition of a.

For each attributed derivation tree, we note a t b iff their exist a
path using direct dependencies from b to a. We denote a t b iff their is no
path.

It is welknown [Kn 71, Lo 74] that it is possible to have a t b and
a b for different derivation trees t1 and t2, and some occurrences of two
attributes a and b in the same rule. This does not necessarily introduce cycle
in the attributes definitions.

From the algorithms of Lohro-Pair [LP 75] it is possible to construct the
relation DS, so defined : a DS b (stable dependency) ↙ V t, a b

If the attribute definitions don't have any cycle (i.e for all attributes
V t not a t a), then for each rule, the DS relation is a partial order relation,
including direct dependencies. Then $B_{r,a} = \{b \mid a \text{ DS } b\}$ satisfies the required
conditions for the proof inference and realise the extention of the direct
dependencies. This solution increases the total number of hypotheses that can
be used.

Not that the termination of the proof results from the finiteness of the
syntactic tree of a finite sentence and from the coherency of the description
by attributes.

We call driving-attributes-network the restriction of DS to the driving-
attributes. The network is the set of all sub-networks of all the rules.

The technique of synthesis is immediately derived from the proof technique :
It uses the same proof scheme, but with fewer definitions, Def<sub>r</sub>. That is :

$$
\forall A_b \ A_{b'} \ \& \ Def'_{r'} \ \& \ ?Def_r : \rightarrow \ A_a \quad (2)
$$

b \in Br, a

where ?Def<sub>r</sub> is the set of the unknown definitions (Def'<sub>r</sub> ∧ ?Def<sub>r</sub> = Def<sub>r</sub>).

To solve this scheme we can recursively replace the defined attributes
(Def'_r definitions) by their definitions and try to identify unknown definitions
as missing hypotheses (?Def_r) to complete the proof. In the definitions
synthesis it is necessary to use all the proof schemes of the rule.
Proof and synthesis will use the same driven-attribute-network.

## Section 2: Specification of a mini-compiler.

We want to completely specify a mini-compiler giving only a part of the attributes definitions and some assertions relating all the attributes between them.

Our mini-compiler analyses Lisp-Like functions $(\lambda xy.(plus x y))$. The syntax of the source language is given in Appendix 1. The object language corresponds to a machine with an unbounded stack of registers and only three instructions : push, pop and link. When a function is called, its arguments are allways in the top registers and its result is pushed on the stack. The semantics of the instructions are described in Appendix 2.

To simplify this example, only the modifications of the stack will be considered.

The specifications of the compiler use four driving-attributes with their definitions : $v^N$, $N = Va$ the variables list of the list $Va$ ; $bv^N$, $N = Fo, LFo, Fu$, the set of the bound variables of scope over $N$ ; $c^N$, $N = Fo, LFo, Fu$, the generated code. of $N$, and $ar^{Fu}$. All the definitions are given in Appendix 3.

From these attributes we can define the others using the following assertions :

$A_v^N : nv^N = lg(v^N)$, i.e $nv^N$ is the length of the list $v^N$.

$B_v^N : ts^N = \{<v_i^N, b^N + i> \mid 1 \le i \le nv^N\}$ i.e $ts^N$ is the set of all pairs <declared variable, location in the stack>, i.e the symbol tables of $Va$. The location in the stack is counted from the bottom of the stack and equals the deepmost argument location (-1) plus the rank of the i-th variable.

$C_{bv}^N : \langle x, i \rangle \in ta^N \supset (x \in bv^N \wedge i \le h^N), N = Fo, LFo, Fu \\ \langle x, i \rangle \in ts^N \supset (x \in \text{set}(v^N) \wedge i \le b^N + nv^N), N = Va$.

Where i is littler than the number of elements in the table ta or the partial table ts, assuming that the number of elements in the table ta allways equals the rank of the topmost stack element ($h^N$).

The property $C_{bv}^N$ gives some indications about the symbol-table : for all pairs of the table the variable (first element of the pair) is bound, and the place pointed by its location is below the topmost stack element of location $h^N$, for the scope $N$. It is a manner to indicate that, where $ta^N$ is incremented with the $ts^N$ elements, the actual locations are preserved. This comes from the constant increasing of the stack size when evaluating an expression. This fact is described by the two following properties :
$D_c^N : h = a \{c^N\} h = a+1, N = Fo, Fu$ (Hoare notations [Ho 69])

$h = a \{c^N\} h : a+na^N, N = LFo$ where h is the rank (counted from the bottom) of the topmost stack element.

$E_c^N : h = h^N \{c^N\} h = s^N, N = Fo, Fu, LFo$

$D$ indicates that only one or $na^{LFo}$ results are accumulated at the top of the stack after the evaluation of an expression (Fo), a function (Fu) or a list of arguments (LFo). $D$ introduces the definitions of $na$ with regard to $c$. $E$ introduces the definitions of $h$ and $s$, which are the heights of the stack before and after the execution of the object code corresponding to $N(c^N)$.

So the properties $A, B, C, D$, and $E$ specify the attributes $nv, ts, ta, b, h, s, na$ from $v, bv, ar$ and $c$. We remark that some of the attributes are better specified than others : $nv$ and $ts$ are completely defined by $A$ and $B$ - their definition may be automatically synthetized - but $ar$ and $ta$ are less defined by $B$ and $C$. In fact $C$ does not often permit the automatic synthesis of $ta$ (It is possible for identities), but we may consider that a description satisfying the previous five properties is partly correct. We are in fact certain that the results (whose correctness was not controlled here) are at the right locations and that the addresses calculations verify properties preserving their validity.

## Section 3 : Synthesis of the missing definitions

Attributes $v, bv, ar$ and $c$ with their definitions form a driving-attribute-network. The $DS$ relation is here reduced to the direct dependencies (section 1). Figure 1 shows the network corresponding to rule 1. It happens to be the same when all the definitions are known (figure 2). It would be different if we used $ta$ and $ts$ for $bv$ and $v$ as driving-attributes of $B$ and $C$. Figure 3 shows the new network with $ta$ and $ts$ as $d$-attributes (rule 1).

We consider here the synthesis in rule 1. The definitions of the driving attributes are (Appendix 3) :

$$ 
\begin{array}{l@{\quad}l@{\quad}l}
\text{Fo} = (\text{Fu LFo}) & \text{ar}^{\text{Fu}} = \text{na}^{\text{LFo}} & \text{c}^{\text{Fo}} = \text{c}^{\text{LFo}} ; \text{Fu}^{\text{LFo}} ; \text{pop na}^{\text{LFo}} \\
& \text{bv}^{\text{Fu}} = \text{bv}^{\text{Fo}} & \\
& \text{bv}^{\text{1.Fo}} = \text{bv}^{\text{Fo}} &
\end{array}
$$

From the $d$-attribute network we deduce the schemes of the proofs of $A, B, C, D$ and $E$ for the rule 1 (Appendix 4).
<figure><img src="image_3.png" /><figcaption>Figure 1. Driving-attributes network for the rule 1.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 2. DS relation in rule 1. Only direct dependencies and DS among the non-terminal symbols are indicated.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Figure 3. Driving-attributes network with ta and c as attribute symbols.</figcaption></figure>
$$1. \quad D_c^{Fu} \wedge D_c^{LFO} \wedge E_c^{Fu} \wedge E_c^{LFO} \quad \rightarrow \quad D_c^{Fo}$$

$$2. \quad " \quad " \quad " \quad " \quad \rightarrow \quad E_c^{Fo}$$

$$3. \quad C_{bv}^{Fo} \quad \rightarrow \quad C_{bv}^{LFO}$$

$$4. \quad " \quad \rightarrow \quad C_{bv}^{Fu}$$

The synthesis we want to obtain are the following :

$$h^{LFO} = h^{Fo}$$

$$s^{Fo} = s^{Fu} - na^{LFO}$$

$$h^{Fu} = s^{LFO}$$

$$ta^{LFO} = ta^{Fo}$$

$$ta^{Fu} = ta^{Fo}$$

The schemes 1-4 are used for the synthesis (Def¹, the definitions of the d-attributes are omitted here to simplify the presentation). For this rule the first scheme does not induce any definition, because na is defined only at a right non-terminal symbol and consequently not defined in this rule (na is synthetized). We will show here how the second scheme induces the definitions of h and s. The hypothesis $D_c^{Fu}$ and $D_c^{LFO}$ are not useful and consequently not reproduced here. The scheme 2 gives the following implication :

$$\begin{align*} h &= h^{Fu} \{c^{Fu}\} \quad h = s^{Fu} \wedge h = h^{LFO} \{c^{LFO}\} \quad h = s^{LFO} \\ \Rightarrow h &= h^{Fo} \{c^{LFO} ; c^{Fu} ; \text{pop } na^{LFO}\} \quad h = s^{Fo} \end{align*}$$

where the underlined attributes correspond to the attributes being defined. The two elements of code $c^{Fu}$ and $c^{LFO}$ may be composed in the same order as the right member using the axiom of composition. This composition is possible iff $h^{Fu} = s^{LFO}$, and gives : $h = h^{LFO} \{c^{LFO} ; c^{Fu}\} h = s^{Fu}$.

Using the definition of pop i (Appendix 2), we can compose pop na$^{LFO}$ with the precedent result, that is :

$$h = h^{LFO} \{c^{LFO} ; c^{Fu} ; \text{pop } na^{LFO}\} h = s^{Fu} - na^{LFO}$$

so as to compare it to the right member of the implication. To complete the proof it is possible to take : $h^{LFO} = h^{Fo}$ and $s^{Fo} = s^{Fu} - na^{LFO}$. Thus we obtain the definitions :

$$h^{LFO} = h^{Fo}$$

$$s^{Fo} = s^{Fu} - na^{LFO}$$

$$h^{Fu} = s^{LFO}$$
we can induce likewise, with the schemes 3 and 4, using the already obtained definitions and the simplest rule of identification, on the other definitions :

$$ \begin{aligned} \text{ta}^{\text{LFO}} &= \text{ta}^{\text{FO}} \\ \text{ta}^{\text{FU}} &= \text{ta}^{\text{FO}} \end{aligned} $$

Note that to obtain the two last results it is necessary to use two heuristics. The first corresponds to the fact that commonly we are looking for identities and that the simplest is generally the best. The second indicates that in certain cases it is possible to use independently proved properties, (with independent d-a-network). To synthetize the last definition ($\text{ta}^{\text{FU}} = \text{ta}^{\text{FO}}$) we need to use the fact that : $s^{\text{LFO}} = h^{\text{LFO}} + na^{\text{LFO}}$, i.e $s^{\text{LFO}} \ge h^{\text{FO}}$ deduced from C and E. Another point is that insufficient specifications may generate false or incomplete definitions.

## Conclusion

The synthesis mechanism is like the proof mechanism, but it seems more difficult to perform. In fact, for the second we know all the attributes definitions, which permit to build a richer driving-attributes network, and for the first one we have a supplementary step of induction (unknown definitions) with the risk to synthetize false definitions. We have shown in [Der 78b] that in certain cases such as the synthesis of nv and ts in the mini-compiler, the synthesis corresponds to a logical deduction from the assertions.

It is thus possible to realize an automatized system to synthetize attributes definitions which runs in two steps : first it constructs the driving-attributes-network. Then it try to deduce or induce the missing definitions, and complete its work through proofs. Eventually it is necessary to test the coherency of the new system of attributes definitions. This is already done automatically.
References

[ANP 78] M. AMIRCHAHY, D. NEEL, C. PAIR, "Correctness Proof of System Directed Processing Descriptions by Attributes", to be published in Journal of Computer and System Sciences.

[Bo 72] G.V. BOCHMANN, "Semantic evaluation from left to right", CACM 19(2), pp 55,62, Feb. 1972.

[Bor 75] J. BOROWIEC, "Programatics in a compiler producing system", Institute of Mathematical Machine, PERA, Warsaw, July 1975.

[CM 75] L.M. CHIRICA, D.F. MARTIN, "An Approach to Compiler Correctness". Sigplan Notices Vol 10, N° 6, p 96, June 1975.

[CM 77] L.M. CHIRICA, D.F. MARTIN, "An Algebraic formulation of Knuthian Semantics". U. of California, Los Angelès, CSD, 1977.

[De 78a] P. DERANSART "Technique de preuve par attributs appliquée à un compilateur Lisp". RR n° 271. IRIA Laboria, Jan. 1978 (French).

[De 78b] P. DERANSART "Preuve et génération d'attributs sémantiques". AFCET Congress 11-13 Nov. 1978 (French).

[Fa 72] I. FANG, "FOLDS, a Declarative Formal Language Definition System", CSD Stanford U., Palo Alto, California, STAN-CS. 329, Dec. 1972.

[GRW 77] H. GANZINGER, K. RIPKEN, R. WILHELM, "Automatic Generation of optimizing multipass compiler", Information Processing 74, G. GILCHRIST Ed., IFIP, North Holland publishing Company, 1977.

[Ho 69] C.A.R. HOARE, "An axiomatic basis for computer programming", CACM 12, n° 10, pp 576,581, 1969.

[JP 77] M. JAZAYERI, D. POZEFSKY, "Algorithms for efficient evaluation of multi-pass attribute grammars without a parse tree", DCS, U. of North California, Chapel Hill, TR 77-001, Feb. 1977.

[Kn 68] D.E. KNUTH, "Semantics of CFL", Math. Syst. Theory, 2,2,1968

[Kn 69] D.E. KNUTH, "The art of computer programming, V1, Addison Wesley Pub. Company, 1969.

[Kn 71a] D.E. KNUTH, "Semantics of CFL", Corrigenda. Math. Syst. Theory 5, pp 95, 96, 1971.
[Kn 71b] D.E. KNUTH, "Examples in Formal Semantics", lectures Notes in Math. n° 188, Springer Verlog, Berlin 1971, pp 212-235.

[Ko 74] C.H.A. KOSTER, "Using the CDL compiler compiler" in : F.L. Bauer and J. Eickel Eds. Compiler construction - an advanced course, Lecture Notes in Comp. Science, V21, Springer Verlag, pp 366, 426, 1974.

[LB 74] O. LECARME and G.V. BOCHMANN, "A truly usable and portable compiler writing system, Information Processing, pp 218, 221, 1974.

[Lo 74] B. LORHO, "De la Définition à la Traduction des Langages de programmation : méthode des attributs sémantiques", Thèse d'Etat, U. Paul Sabatier, Toulouse 1974 (French).

[Lo 71] R.L. LONDON, "Correctness of two compilers for a Lisp Subset. CSD report n° CS240, Stanford U., October 1971.

[LP 75] B. LORHO, C. PAIR, "Algorithms for checking the consistency of attribute grammars". Colloque IRIA, 1-3 July, Arc et Senans, France.

[N.A. 74] D.NEEL, M. AMIRCHAHY, "Semantic Attribute and Improvement of Generated Code", ACM 74, Nov, 11-13 San Diego, California 1974.

[Nc 75] D. NEEL, "Contribution à la formalisation de l'amélioration du code par attributs sémantiques", Thèse d'Etat, U. de Paris 6, 1975 (French)

[W 71] W.T. WILNER, "Declarative Semantic Definition", CSD, Stanford U., Palo Alto, California, STAN-C3 233-71, 1971.

[Wi 75] R. WILHELM, "Code optimierung mittels attributierter transformations grammatiken", Lectures Notes in Comp. Sciences 26, Springer Verlag, pp 257, 266, 1975 (German)
# Appendix 1 Source language syntax

0. $F = (\lambda Va . Fo)$

1. $Fo = (Fu LFo)$

2. $Fo = Id$

3. $LFo = Fo LFo$

4. $LFo = \epsilon$ (empty string)

5. $Fu = (\lambda Va . Fo)$

6. $Fu = Id$

7. $Va = Va Id$

8. $Va = Id$

$Va$ : List of variables

$Fo$ : Form (Expression)

$LFo$ : List of forms

$Fu$ : Function

$Id$ : Identifier

# Appendix 2 Objet language semantics.

Hoare notations [Ho 69]

push $h = a$

$h = a+1$

$h$ : height of the stack

oc = b {push i}

oc = b+1

$c(h)=c(h-i)$

oc : ordinal counter

pop $h = a$

$h = a-n$

$c(j)$: content of the place of location j in the stack

oc = b {pop n}

oc = b+1

$c(h)=d$

$c(h)=d$

link $h = a$

$h = a+1$

oc = b

{link Id,n}

oc = b+1

.a = list(c(h-n+1)..c(h))

c(h) = results of applying la to function Id.

P1 {C1} Q1 ^ Q1 {C2} Q2

composition axiom

P1 {C1 ; C2} Q2

# Appendix 3 Mini-compiler description.

a - Used attributes and non-terminals where they are defined :

<table><thead><tr><th>inherited</th><th>non-terminal</th><th>synthetised</th></tr></thead><tbody><tr><td></td><td>F</td><td>c</td></tr><tr><td>h, ta, bv</td><td>Fo</td><td>c, s</td></tr><tr><td>h, ta, bv</td><td>LFo</td><td>c, s, na</td></tr><tr><td>ar, h, ta, bv</td><td>Fu</td><td>c, s</td></tr><tr><td>b</td><td>Va</td><td>ts, nv, v</td></tr></tbody></table>

where

code $c^N$

$h^N, s^N$ respectively heights before and after execution of generated

$ta^N, ts^N$ symbols table of bounded variables set $bv^N$ and list $v^N$.

$na^N, ar^N$ number of arguments of a function

$nv^N$ number of elements of $v^N$

$b^N$ location in the stack of the first argument of a function.
Appendix 4 Schemes of proofs. (', ' denotes conjunction)

0. $D_c^{Fo}, E_c^{Fo} \rightarrow D_c^F, E_c^F$

1. $D_c^{Fu}, D_c^{LFe}, E_c^{Fu}, E_c^{LFe} \rightarrow D_c^{Fo}, E_c^{Fo}$

$C_{bv}^{Fo} \rightarrow C_{bv}^{LFe}, C_{bv}^{Fu}$

2. $\rightarrow D_c^{Fo}, E_c^{Fo}$

3. $D_c^{Fo}, D_c^{LFe}, E_c^{Fo}, E_c^{LFe}' \rightarrow D_c^{LFe}, E_c^{LFe}$

$C_{bv}^{LFe} \rightarrow C_{bv}^{Fo}, C_{bv}^{LFe}'$

4. $\rightarrow D_c^{LFe}, E_c^{LFe}$

5. $D_c^{Fo}, E_c^{Fo} \rightarrow D_c^{Fu}, E_c^{Fu}$

$A_v^{Va}, B_v^{Va}, C_v^{Va}, C_{bv}^{Fu} \rightarrow C_{bv}^{Fo}$

6. $\rightarrow D_c^{Fu}, E_c^{Fu}$

7. $A_v^{Va'}, B_v^{Va'}, C_v^{Va'} \rightarrow A_v^{Va}, B_v^{Va}, C_v^{Va}$

8. $\rightarrow A_v^{Va}, B_v^{Va}, C_v^{Va}$