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

HAL
open science

# Semantics of procedures as an algebraic abstract data type

Marie-Claude Gaudel, Monique Mazaud, Philippe Deschamp

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

## To cite this version:

Marie-Claude Gaudel, Monique Mazaud, Philippe Deschamp. Semantics of procedures as an algebraic abstract data type. [Research Report] IRIA-RR-334, IRIA. 1978, pp.24. hal-04716543

HAL Id: hal-04716543

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

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_3.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

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

SEMANTICS OF PROCEDURES
AS AN ALGEBRAIC
ABSTRACT DATA TYPE

Marie-Claude GAUDEL
Philippe DESCHAMP
Monique MAZAUD

Rapport de Recherche N° 334

Décembre 1978
SEMANTICS OF PROCEDURES AS AN ALGEBRAIC ABSTRACT DATA TYPE

Marie-Claude Gaudel, Philippe Deschamp, Monique Mazaud

Résumé :

Nous proposons d'utiliser les types abstraits algébriques pour formuler la sémantique des langages de programmation. Nous présentons l'exemple réaliste d'un langage comportant des procédures récursives et des variables globales. On obtient un modèle simple de la sémantique d'un tel langage. L'intérêt de cette approche est qu'elle permet de spécifier et de prouver des compilateurs.

Abstract :

Algebraic abstract data types can be used as a framework to formalize the semantics of programming languages.

We give here an example of a language with recursive procedures and global variables. This approach allows to specify and prove compilers.
## Introduction

This paper presents a formal semantics of programming languages which is used to specify and construct compilers.

The semantic value of a program is a formula of some algebraic abstract data type [Guttag 76]. This formula can be considered as a program scheme [Courcelle 78] and then this semantics could be called "algebraic". It could also be considered as "denotational" [Tennent 76], for the formula which is obtained denotes a modification, i.e. can be interpreted as some function from state to state ...

However the problem of which adjective is used as a characterization is not very important with regard to our actual aim : to specify, prove and produce compilers, using some recent results on the representation of algebraic abstract data types. Our approach has already been introduced in [Gaudel 77] where a small translator is studied : the semantics of the source language and of the target language are both described with the same formalism. Then the representation of the semantic values of the source programs in terms of semantic values of target programs is specified and proved as the representation of an algebraic abstract data type by another one.

The specific goal of this paper is to show, by way of two examples, what the semantics of usual programming languages looks like in our formalism.

The first example is an extension of the source language studied in [Gaudel 77]. Its control structures are simple and its data structures are (a little) more complicated. The purpose of this part of the paper is to familiarize the reader with our notations and the theory.

The other language is more realistic : it allows the use of recursive procedures with parameters by value and by reference. This language is very close to the one studied in [Apt 77] with the denotational approach. In [Gaudel 79a, Deschamp 79] the interested reader will see how to deal with functions, with procedures and functions as parameters and with by-name parameters "à la Algol 60".
# I. THE FLEXSEQ LANGUAGE

By way of introduction we will consider a simple language where the only data types are integers and integer sequences. A sequence is of flexible length. When a sequence identifier is declared, the value of the length of the sequence is initialized to zero.

The operations for sequences are : **extend** the sequence by appending a new integer item ; **retract** the sequence by deleting the last item ; **select** or **change** the value of the i-th item. Usual integer and boolean expression are also available.

The syntax of FLEXSEQ is given below.

*   `<P>` → `<DL>` ; `<SL>`
*   `<DL>` → `<DL>` ; `<D>` | `<D>`
*   `<D>` → **integer ID** | **sequence ID**
*   `<SL>` → `<SL>` ; `<S>` | `<S>`
*   `<S>` → **extend** (`ID`, `<E>`) | **retract** (`ID`) | `ID` := `<E>` |
    ID [<E>] := <E> |
    **if** <C> **then** <SL> **else** <SL> **fi** |
    **while** <C> **do** <SL> **od**
*   `<E>` → `<E>` `<OP1>` <T> | <T>
*   <T> → (<E>) | `ID` | `INT` | `ID` [<E>] | **length** (`ID`)
*   `<OP1>` → `+` | `-` | `*` | `%`
*   `<C>` → `<C>` `<OP2>` <B> | <B>
*   <B> → (<C>) | `<E>` `<REL>` <E>
*   `<OP2>` → **or** | **and**
*   `<REL>` → `=` | `≠` | `<` | `≤` | `>` | `≥`

## I.1 EXPRESSIONS

To formalize the semantics of FLEXSEQ expressions we first give the name of the types and of the operations on them which occur in the semantic description. Their properties are then specified, i.e. their domains, co-domains and algebraic axioms.

In this simple case, the types are directly deduced from the FLEXSEQ data types : Sequence Identifiers, Integer Identifiers, Integers, Booleans. The names of types and operations are listed below :
type seq-id, int-id, int, bool ;

operations

(seq-id) → int : size ;

(seq-id, int) → int : ith ;

(int-id) → int : value of ;

(int, int) → int : plus, sub, times, div ;

(int, int) → bool : eq, neq, lt, le, gt, ge ;

(bool, bool) → bool : or, and ;

axioms

(The usual axioms for integers and booleans are assumed. For instance :)

for x, y ∈ int :

plus (x, int '0') = x

plus (x, plus (y, int '1')) = plus (plus (x, y), int '1')

times (x, int '0') = int '0'

times (x, plus (y, int '1')) = plus (times (x,y),x)

lt (x, plus (y, int '1')) = or (lt (x, y), eq (x, y))

and so on.

The constants of a type are enclosed between quotes, preceded by the name of their type. Strictly speaking, they are nullary operators but it is unnecessary to list all of them : we are only interested in formulas and the detailed syntax of constants is irrelevant : we only need the name of the type and the text of the constant.

I.2 STATEMENTS AND MODIFICATIONS

The definitions above allow the description of the semantics of FLEXSEQ expressions. To describe the semantics of elementary or compound statements we introduce a new name of type :

type modif ;

which formalizes the notion of "state modification" : the semantics of a state-
ment is then a formula of type modif.

The operations with modif as co-domain are :
## operations

<table><tr><td>(seq-id) → modif</td><td>: init;</td></tr><tr><td>(seq-id) → modif</td><td>: shorten;</td></tr><tr><td>(seq-id, int) → modif</td><td>: lengthen;</td></tr><tr><td>(seq-id, int, int) → modif</td><td>: alterith;</td></tr><tr><td>(int-id, int) → modif</td><td>: assign;</td></tr><tr><td>(modif, modif) → modif</td><td>: concat;</td></tr><tr><td>(bool, modif, modif) → modif</td><td>: condition;</td></tr><tr><td>(bool, modif) → modif</td><td>: loop;</td></tr><tr><td>() → modif</td><td>: stoperror;</td></tr></table>

These operations are going to be described by means of algebraic axioms. But in order to write these axioms we need some intuitive understanding of what is a state or, more formally, of the mathematical theory of which the abstract data type is a model. In this paper our approach is very informal, a complete theoretical statement of the theory will be found in [Gaudel 79b].

Rather than the word "state", we will use the word "information" [Remy 74]. An information is a set of valid formulas on the expressions of the abstract data type. An instance of such formulas could be:

value of (int-id 'I') = int '3'
ith (seq-id 'S', int '1') = int '2'
value of (int-id 'I') = value of (int-id 'I')
etc.

More precisely, an information is the set of valid formulas which can be deduced from:

- some axioms specific to the information, for instance:

value of (int-id 'N') = int '5';

- some general axioms which are common to all the informations considered.

In our example these axioms are those given in I.1;

- some logical axioms (on equality, implication and so on), for instance:

x = x.

The meaning of a modification "m" is a mapping from the set of informations verifying the general and logical axioms into itself. This is expressed by the operator $app_l$ which has as operands a modification and an information, and which returns an information:

$app_l(m, I) = I'$
Using this operator we can now write axioms for the operators on modifications :

$$
\begin{align*}
\mathit{appl} ( \mathit{concat} (m, m'), I ) &= \mathit{appl} (m', \mathit{appl} (m, I)) \\
( b = \mathit{bool} \ 'true' ) &\in I \supset \mathit{appl} ( \mathit{condition} (b, m, m'), I ) \\
&= \mathit{appl} (m, I) \\
( b = \mathit{bool} \ 'false' ) &\in I \supset \mathit{appl} ( \mathit{condition} (b, m, m'), I ) \\
&= \mathit{appl} (m', I) \\
( b = \mathit{bool} \ 'false' ) &\in I \supset \mathit{appl} ( \mathit{loop} (b, m), I ) = I \\
( b = \mathit{bool} \ 'true' ) &\in I \supset \mathit{appl} ( \mathit{loop} (b, m), I ) \\
&= \mathit{appl} ( \mathit{concat} (m, \mathit{loop} (b, m)), I )
\end{align*}
$$

To define modifications such as *assign* we use an elementary modification *subst*. Its definition is :

$$
P_{\mu}^{\lambda} \in I \Rightarrow P \in appl (subst (\lambda, \mu), I)
$$

Then any modification can be defined in terms of *subst* :

$$
\begin{align*}
\mathit{init} (\mathit{sid}) &= \mathit{subst} (\mathit{size} (\mathit{sid}), \mathit{int} \ '0') \\
\mathit{shorten} (\mathit{sid}) &= \mathit{subst} (\mathit{size} (\mathit{sid}), \mathit{sub} (\mathit{size} (\mathit{sid}), \mathit{int} \ '1')) \\
\mathit{lengthen} (\mathit{sid}, \mathit{v}) &= \mathit{concat} (\mathit{subst} (\mathit{size} (\mathit{sid}), \\
& \qquad \mathit{plus} (\mathit{size} (\mathit{sid}), \mathit{int} \ '1'))), \\
& \qquad \mathit{subst} (\mathit{ith} (\mathit{sid}, \mathit{size} (\mathit{sid})), \mathit{v})) \\
\mathit{alterith} (\mathit{sid}, i, \mathit{v}) &= \mathit{subst} (\mathit{ith} (\mathit{sid}, i), \mathit{v}) \\
\mathit{assign} (\mathit{id}, \mathit{v}) &= \mathit{subst} (\mathit{value\ of} (\mathit{id}), \mathit{v})
\end{align*}
$$

We have defined all the modifications but stoperror. One way to do that is
to write :

$$
\mathit{appl} ( \mathit{concat} (m, \mathit{concat} ( \mathit{stoperror}, m1)), I ) = \mathit{appl} (m, I)
$$

For which we need some associativity axiom for *concat* :

concat ( concat (m, m1), m2) = concat ( m, concat (m1, m2))

subst and appl are sufficient to specify the modifications occuring in the
semantic description of FLEXSEQ. In some more complicated cases, concurrent
substitution is necessary :

$$
P_{\mu_1, \dots, \mu_n}^{\lambda_1, \dots, \lambda_n} \in I \Rightarrow P \in appl ( \text{subst} (\langle \lambda_1, \dots, \lambda_n \rangle, \langle \mu_1, \dots, \mu_n \rangle), I )
$$

For instance

$$
subst (<a, b (a)>, <e, a>)
$$

denotes concurrent substitution of "a" by "e" and of "b(a)" by "a".
In case of ambiguity, the longest formula is replaced : in the above example
"b (a)" is everywhere replaced by "a" and not by "b (e)".

## I.3 DEALING WITH ERRORS

We have not yet considered the error cases, but specification of these cases
must obviously appear in the semantic description of FLEXSEQ. For instance, it
is forbidden to shorten an empty sequence or to access to an element of a
sequence with an index too small or too large.

The problem of errors in abstract data types has already been well studied
[Goguen 77, Guttag 78b]. We use Guttag's solution : when specifying a language
semantics one has to describe the run-time error cases by restriction
specifications. There are two kinds of such specifications : Failure Specifi-
cation or Pre-Condition Specification. Both serve to restrict the domain of
an operation. The difference is that, in the former case, the implementation
is supposed to ensure that the operation is not used with arguments out of this
domain ; in the latter case, the users of the abstract data type (i.e. the people
who specify the language) are in charge of checking or proving that for each
use of the operation the arguments are in the domain.

We are going to show both ways of specifying errors in FLEXSEQ.

### I.3.1 Failure Specifications

For $sid \in seq-id$, $i, v \in int$ :

eq ( size (sid), int '0') => Failure (shorten ; sid)

or ( lt (i, int '1'), gt (i, size (sid)) => Failure (ith ; sid,i)

or ( lt (i, int '1'), gt (i, size (sid)) => Failure (alterith ; sid,i,v)

eq (i, int '0') => Failure (div : v,i)

This specification permits shorten, *ith*, *alterith* to be used in the
semantic function definitions without bothering about checks which will be
performed by the implementation.

### I.3.2 Preconditions

Pre ( shorten ; sid) = neq ( size (sid), int '0') ;

Pre ( ith ; sid,i) = and ( gt (i, int '0'), le (i, size (sid))) ;

Pre ( alterith ; sid,i,v) = Pre ( ith ; sid,i) ;
For each use of *shorten*, *ith* or *alterith*, one has to be sure that the precondition is true : that can be done by proving it in the context of each use or by inserting a check.

## I.4. SEMANTIC FUNCTIONS

These functions map sentences of the language into formulas of the abstract data type we just defined. The type of the formulas depends on the kind of sentence considered. That is the reason why we need three functions :

$S_0 : P \cup DL \cup D \cup SL \cup S \rightarrow$ modification formula

$V_I : E \cup T \rightarrow$ integer formula

$V_B : C \cup B \rightarrow$ boolean formula

At this point we take into account only correct programs, i.e. programs where the identifiers are declared and used properly. We consider that the restrictions have been specified as in I.3.1, i.e. using Failure cases. Then the semantics of FLEXSEQ is :

$S_0[DL; SL] = concat(S_0[DL], S_0[SL])$

$S_0[DL; D] = concat(S_0[DL], S_0[D])$

$S_0[integer ID] = \epsilon$

$S_0[sequence ID] = init(seq-id 'ID')$

$S_0[SL; S] = concat(S_0[SL], S_0[S])$

$S_0[extend (ID, E)] = lengthen (seq-id 'ID', $V_I[E])$)

$S_0[retract (ID)] = shorten (seq-id 'ID')$

$S_0[\text{ID} := E] = \text{assign} (\text{int-id 'ID', } V_I[E])$

$S_0[\text{ID}[E}_1] := E_2] = \text{alterith} (\text{seq-id 'ID', } V_I[E_1], V_I[E_2])$

$S_0[\text{if C then } SL_1 \text{ else } SL_2 \text{ fi}] = \text{condition} (V_B[C], S_0[SL_1], S_0[SL_2])$

$S_0[\text{while C do SL od}] = \text{loop} (V_B[C], S_0[SL])$

$V_I[E + T] = \text{plus} (V_I[E], V_I[T])$

$V_I[(E)] = V_I[E]$

$V_I[\text{ID}] = \text{value of (int-id 'ID')}$
<table>
  <tr>
    <td>υ<sub>I</sub>[INT]</td>
    <td>= int 'INT'</td>
  </tr>
  <tr>
    <td>υ<sub>I</sub>[ID [E]]</td>
    <td>= ith (seq-id 'ID', υ<sub>I</sub>[E])</td>
  </tr>
  <tr>
    <td>υ<sub>I</sub>[length (ID)]</td>
    <td>= size (seq-id 'ID')</td>
  </tr>
  <tr>
    <td>υ<sub>B</sub>[C <u>or</u> B]</td>
    <td>= or (υ<sub>B</sub>[C], υ<sub>B</sub>[B])</td>
  </tr>
  <tr>
    <td>υ<sub>B</sub>[E<sub>1</sub> ≤ E<sub>2</sub>]</td>
    <td>= le (υ<sub>I</sub>[E<sub>1</sub>], υ<sub>I</sub>[E<sub>2</sub>])</td>
  </tr>
</table>

and so on, for the other arithmetic operators, boolean operators and relation symbols.

Note that, in the third equation we use the symbol $\epsilon$ to denote the identity modification, i.e :

$$app_2 (\epsilon, I) = I.$$

The semantic functions are slightly different when the restrictions are specified as preconditions. Let us note $S_1$, $V_J$ and $V_B$ these functions. $S_1$ is different from $S_0$ in the following cases :

$S_1 [[\underline{retract} (ID)]] = \text{condition} (\text{neq} (\text{size} (\text{seq-id 'ID'}), \text{int '0'}), \text{shorten} (\text{seq-id 'ID'}), \text{stoperror})$

$S_1 [[\text{ID}[E_1]] := E_2]] = \text{condition} (\text{and} (\text{gt} (V_J [E_1], \text{int '0'}), \text{le} (V_J [E_1], \text{size} (\text{seq-id 'ID'}))), \text{alterith} (\text{seq-id 'ID'}, V_J[E_1], V_J[E_2]), \text{stoperror})$

The definition of $V_J$ differs from $V_I$ in the case of $V_J[[\text{ID}[E]]]]$. The formula would be a conditional operation with an erroneous result if the precondition is false. In order to write it, we would need to introduce two new operations and their axioms in the abstract data type. That should be quite straightforward.

The semantic value of every program in FLEXSEQ is now defined as a formula which denotes a modification. The properties of such formulas are expressed as axioms. This approach allows numerous possibilities : to prove the validity of some program transformations, to find interesting properties of some programs. Our aim here, which seems the most promising consequence of this study, is to prove translations of these formulas and thereby the correctness of compilers.

In the next section we show that this formalism allows to express in a simple and rigorous way the semantics of procedures, including global variables references and parameter binding.
## II. THE SIMPROC LANGUAGE

The SIMPROC Language is an usual Algol-like programming language with declarations of simple variables, arrays and procedures. Simple and mutual recursivity is allowed. Procedure parameters can be passed by value or as variables. The statements are : assignment, procedure call, sequential composition and conditional composition. A syntax of this language is given below.

```
<P>      -> <DL>; <SL>
<DL>     -> <DL>; <D> | <D>
<D>      -> integer ID | array ID [INT] | ε
          proc ID (val ID, var ID)
          begin <DL>; <SL> end
<SL>     -> <SL>; <S> | <S>
<S>      -> <VAR> := <E> | call ID (<E>, <VAR>) |
          if <E> eq <E> then <SL> else <SL> fi
          <E> + <T> | <E> - <T> | <E> * <T> |
          <E> % <T> | <T>
<T>      -> <VAR> | (<E>) | INT
<VAR>    -> ID | ID [<E>]
```

For simplicity we consider that every procedure has exactly two parameters : the first one passed by value, the second one as a variable. Furthermore, all declared identifiers are assumed to be different : if necessary they should be renamed in some way. As before only valid programs are taken into account.

### II.1 TYPES AND OPERATIONS

We shall at first introduce the main types and operators, together with their axioms and preconditions. The full definition of the abstract data type will follow.

#### II.1.1 Intuitive Introduction

**a) Identifiers**

The identifier types are directly deduced from the SIMPROC data types :

types var-id, array-id, proc-id, ref-id;

the type ref-id is used for parameter identifiers passed as variables.
Some operations are defined on the union of these types. Then we need to
introduce the type *id* :

`type id = union (var-id, array-id, proc-id, ref-id);`

`operations`

`(id) -> proc-id : father ;`

`(proc-id) -> var-id : param1 ;`

`(proc-id) -> ref-id : param2 ;`

The *father* operation gives for any identifier the *identifier* of the procedure to which it is local. Parameter identifiers are associated to each procedure identifier by the operations *param1* and *param2*.

For example, for the program below :

`integer I;`

`proc F (val X, var Y)`

`begin`

`array A[10];`

`proc G(val U, var V)`

`begin`

`integer J ;`

⋮

`end ;`

⋮

`end ;`

⋮

we have among others, the following formulas :

`father (var-id 'J') = proc-id 'G'`

`param1 (proc-id 'G') = var-id 'U'`

`param2 (proc-id 'G') = ref-id 'V'`

`father (proc-id 'G') = proc-id 'F'`

`father (array-id 'A') = proc-id 'F'`

`father (proc-id 'F') = proc-id 'PROG'`

`father (var-id 'I') = proc-id 'PROG'`

Among the general axioms are :

`for p-id ∈ proc-id :`

`father (param1 (p-id)) = p-id`

`father (param2 (p-id)) = p-id`
In the above example, we use the procedure identifier `PROG` as the value of `father` for identifiers declared at program level. This identifier is a special one which is associated with the program. We have to state the two following properties :

- there is no procedure to which `PROG` is local ;

- every identifier used must be a descendant of `PROG`. (1)

Hence the following preconditions :

`for id1, id2 in id:`

`Pre (father ; id1) = (id1 ≠ proc-id 'PROG')`

`Pre (id1) = ANCESTOR (proc-id 'PROG', id1) v (id1 = proc-id 'PROG')`

where

ANCESTOR(id1, id2) = 
    if id2 = proc-id 'PROG'
    then FALSE
    elseif father (id2) = id1
    then TRUE
    else ANCESTOR (id1, father (id2))

Notice that `ANCESTOR` as well as `if ... then ... else ...`, `v =, =, =, ...` is a symbol of the logical language used to write axioms and preconditions.

## b) Calls

One of the most difficult issues encountered when describing such a language is that a variable identifier, local to a procedure, refers to a different variable for each call of that procedure. In addition, we want to be able to specify which variable is refered to by an identifier non-local to the current procedure. To deal with this problem we shall introduce the types variables and calls of procedures and some operators which, given an identifier and a call, yield a variable.

We now focus our attention on the operations and axioms for procedure calls and procedure identifiers.

`type call ;`

`operations`

( ) -> call : current call ;

(call) -> call : caller ;

(call) -> proc-id : name ;

<footnote>(1) In other words, the only identifiers for which the axioms and preconditions are relevant are those occuring in the program text.</footnote>
An example of the relationship between them is illustrated by the figure below :

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

where 'x' stands for a call and '.' stands for a procedure identifier.

An important property is that all the calls in the chain are different. (Some procedure identifiers are possibly the same, as recursive calls are allowed).

We then have the following axioms :

for c1, c2 ∈ call :

caller (c1) = caller (c2) ⇒ c1 = c2

caller (c1) ≠ current call

The oldest call in the chain is that of the program. Its name is the procedure identifier PROG. This is specified by the precondition :

Pre (caller ; c1) = (name (c1) ≠ proc-id 'PROG')

The latest call is designated by the nullary operation current call .

c) Variables

We present now the operators which, given an identifier and a procedure call, yield a variable.

At first we study the case of a simple variable identifier. Then we specify the operators for the identifiers of parameters passed as variables. The operator and axioms for the array identifiers are not given here. They can be found in the full definition of the abstract data type in II.1.2.

In the case of a simple variable identifier we have :

type var ;

operations

(var-id, call) → var : appoints ;

(var) → int : value of ;

The properties of the operator appoints are :

1) appoints gives a different result for each couple <id, c> such that id is local to the procedure call c, i.e :
(id1 ≠ id2 ∨ c1 ≠ c2) ∧ (name (c1) = father (id1)) ∧ (name (c2) = father (id2)) →
appoints (id1, c1) ≠ appoints (id2, c2)

This first axiom expresses the "creation" of new local variables for every
procedure call.

2) for a couple <id, c> such that id is not local to the procedure call c
(i.e. id is a global identifier), *appoints* yields the same result as for the
"previous" call :

name (c1) ≠ father (id1) → appoints (id1, c1) = appoints (id1, caller(c1))

Of course, there is a precondition for *appoints* which expresses the scope rules
in Algol-like languages :

Pre (*appoints* ; id1, c1) = (father (id1) = name (c1))

v ANCESTOR (father (id1), name (c1))

Hence the meaning of a simple variable identifier ID is the following formula of
type *var* :

appoints (var-id 'ID', current call)

except in some particular cases, e.g. the use of a parameter passed as a varia-
ble. In this case the formula is :

ref-appoints (ref-id 'ID', current call)

where *ref-appoints* is very simular to *appoints*. The main difference is that its
co-domain is the type *ref-var*. This type describes the variables which refer to
other variables, which have integer as value.

type ref-var ;

operations

(ref-id, call) → ref-var : ref-appoints ;

(ref-var) → var : refers-to ;

The axioms and precondition related to *ref-appoints* are very close to those of *appoints*, and will be found in II.1.2.

d) Modifications

Continuing the description of types and operations, we now introduce a
type *modif* as in the previous example. The value of a procedure identifier is
of type *modif*. This value is expressed by the operation *possesses*.
type modif ;

operations

(proc-id) → modif : possesses ;

Among the other operations on modifications are :

(modif, modif) → modif : concat ;

(int, int, modif, modif) → modif : condit ;

(var, int) → modif : assign-int ;

(ref-var, var) → modif : assign-var ;

The axioms for concat are the same as in the first part.

For the conditional we have :

for i, j ∈ int, m1, m2 ∈ modif :

(i = j) ∈ I → appl (condit (i, j, m1, m2), I) = appl (m1, I)

(i = j) & I → appl (condit (i, j, m1, m2), I) = appl (m2, I)

assign-int and assign-var are defined by :

for v ∈ var, i ∈ int, rv ∈ ref-var :

assign-int (v, i) = subst (value of (v), i)

assign-var (rv, v) = subst (refers to (rv, v))

We shall define the other modifications in the course of describing the semantic functions.

II.1.2 Definition of the abstract data type.

One can find in this section all the operations, axioms and restrictions used to write the semantic functions. However some modifications are defined in the next part.

The operators and axioms not yet specified are easy to understand.

type proc-id, var-id, array-id, ref-id, var, ref-var, int, call, modif ;

type id = union (proc-id, var-id, array-id, ref-id) ;

operations

(id) → proc-id : father ;

(proc-id) → var-id : param1 ;

(proc-id) → ref-id : param2 ;

(proc-id) → modif : possesses ;

(var-id, call) → var : appoints ;

(ref-id, call) → ref-var : ref-appoints ;

(ref-var) → var : refers to ;

(var) → int : value of ;

(array-id) → int : upperbound ;

(array-id, call, int) → var : element ;
<table><tr><td>( )</td><td>→ call : current call;</td></tr><tr><td>(call)</td><td>→ call : caller;</td></tr><tr><td>(call)</td><td>→ proc-id : name;</td></tr><tr><td>(int, int)</td><td>→ int : plus, sub, mult, div;</td></tr><tr><td>(var, int)</td><td>→ modif : assign-int;</td></tr><tr><td>(ref-var, var)</td><td>→ modif : assign-var;</td></tr><tr><td>(modif, modif)</td><td>→ modif : concat;</td></tr><tr><td>(int, int, modif, modif)</td><td>→ modif : condit;</td></tr></table>

### Axioms

for pid ∈ proc-id, vid1, vid2, ∈ var-id, rid1, rid2 ∈ ref-id,
aid1, aid2 ∈ array-id, v ∈ var, rv ∈ ref-var, c1, c2 ∈ call, i, j ∈ int;

father (param1 (pid)) = pid

father (param2 (pid)) = pid

(vid1 ≠ vid2 ∨ c1 ≠ c2) ∧ (name (c1) = father (vid1)) ∧
(name (c2) = father (vid2)) →
  appoints (vid1, c1) ≠ appoints (vid2, c2)

name (c1) ≠ father (vid1) →
  appoints (vid1, c1) = appoints (vid1, caller (c1))

(aid1 ≠ aid2 ∨ i ≠ j ∨ c1 ≠ c2) ∧ (name (c1) = father (aid1)) ∧
(name (c2) = father (aid2)) →
  element (aid1, c1, i) ≠ element (aid2, c2, j)

name (c1) ≠ father (aid1) →
  element (aid1, c1, i) = element (aid1, caller (c1), i)

appoints (vid1, c1) ≠ element (aid1, c2, i)

(rid1 ≠ rid2 ∨ c1 ≠ c2) ∧ (name (c1) = father (rid1)) ∧
(name (c2) = father (rid2)) →
  ref-appoints (rid1, c1) ≠ ref-appoints (rid2, c2)

name (c1) ≠ father (rid1) →
  ref-appoints (rid1, c1) = ref-appoints (rid1, caller (c1))

caller (c1) = caller (c2) → c1 = c2
caller (c1) ≠ current call

(The axioms on integers are the same as in part I)
`assign-int (v, i) = subst (value of (v), i)`

`assign-var (rv, v) = subst (refers to (rv), v)`

`concat (concat (m1, m2), m3) = concat (m1, concat (m2, m3))`

`appl (concat (m1, m2), I) = appl (m2, appl (m1, I))`

`i = j ∈ I → appl (condit (i, j, m1, m2), I) = appl (m1, I)`

`i ≠ j ∈ I → appl (condit (i, j, m1, m2), I) = appl (m2, I)`

## Restrictions

`Pre (father ; id1) = (id1 ≠ proc-id 'PROG')`

`Pre (id1) = ANCESTOR (proc-id 'PROG', id1) v (id1 = proc-id 'PROG')`

`Pre (appoints ; vid1, c1) = (father (vid1) = name (c1)) v ANCESTOR (father (vid1), name (c1))`

`Pre (ref-appoints ; rid1, c1) = (father (rid1) = name (c1)) v ANCESTOR (father (rid1), name (c1))`

`Pre (element ; aid1, c1, i) = (father (aid1) = name (c1)) v ANCESTOR (father (rid1), name (c1)) (upperbound (aid1) < i) v (i ≤ int '0') → Failure (element ; aid1, c1, i)`

`Pre (caller ; c1) = (name (c1) ≠ proc-id 'PROG')`

## II.2 THE SEMANTIC FUNCTIONS

Their domains and codomains are:

`M : P → modification formula`

`S : proc-id × {D U S U DL U SL} → modification formula`

`L : proc-id × VAR → variable formula`

`V : proc-id × {E U T} → integer formula`

The symbols P, D, S, DL, SL, VAR, E and T are those used as non-terminals in the syntax of SIMPROC. The first variable of functions S, L, V identifies the procedure to which the sentence considered is local (1).

<footnote>(1) It is possible to write the semantic functions without this variable. Indeed this identifier can be denoted anywhere by the formula *name* (*current call*). But this last solution leads to inefficient implementations of the languages : the function *name* must then be represented and computed, since its result can only be deduced from the program text.</footnote>
### II.2.1 The function M

$M[DL; SL] = concat(init, concat(S_{PROG}[DL], S_{PROG}[SL]))$

where init is a modification which initializes the chain of calls :

$( ) \rightarrow modif : init;$

$init = subst(name (current call), proc-id 'PROG')$

The notation $S_p[\Upsilon]$ stands for $S(\mathit{proc-id} 'P', \Upsilon)$. It is used in this part of the paper for all the semantic functions.

To improve the intuitive understanding of what is the meaning of a program, one can consider that the results of a program P are the formulas of the information

$appl(M[\Upsilon], I_0)$

where $I_0$ is the information without specific axioms : its only axioms are the general and the logical ones.

### II.2.2 The function S

The semantics of the declarations is given below :

$S_p[DL; D] = concat(S_p[DL], S_p[D])$

$S_p[\underline{integer} ID] = \mathit{decl-int} (\mathit{var-id} 'ID', \mathit{proc-id} 'P')$

where $\mathit{decl-int}$ is defined by

$(\mathit{var-id}, \mathit{proc-id}) \rightarrow \mathit{modif} : \mathit{decl-int};$

$\mathit{decl-int} (\mathit{v-id}, \mathit{p-id}) = \mathit{subst} (\mathit{father} (\mathit{v-id}), \mathit{p-id})$

$S_p[\underline{array} ID[\mathit{INT}]] = \mathit{decl-array} (\mathit{array-id} 'ID', \mathit{int} 'INT', \mathit{proc-id} 'P')$

where :

$(\mathit{array-id}, \mathit{int}, \mathit{proc-id}) \rightarrow \mathit{modif} : \mathit{decl-array};$

$\mathit{decl-array} (\mathit{a-id}, i, \mathit{p-id}) =$
$\mathit{subst} (<\mathit{father} (\mathit{a-id}), \mathit{upperbound} (\mathit{a-id})>, <\mathit{p-id}, i>)$

$S_p[\underline{proc} ID_1 (\underline{val} ID_2, \underline{var} ID_3) \underline{begin} DL; SL \underline{end}] =$

$\mathit{decl-proc} (\mathit{proc-id} 'ID_1', \mathit{var-id} 'ID_2', \mathit{ref-id} 'ID_3', \mathit{proc-id} 'P', concat(S_{ID_1}[DL], S_{ID_1}[SL]))$
where :

(proc-id, var-id, ref-id, proc-id, modif) → modif : decl-proc ;
decl-proc (p-id1, vid, r-id, p, m) =
subst (<father (p-id1), param1 (p-id1), param2 (p-id1),
possesses (p-id1)>, <p, v-id, r-id, m>)

We now state the semantics of statements :

S<sub>p</sub> [[LS ; S]] = concat (S<sub>p</sub> [[LS]], S<sub>p</sub> [[S]])

S<sub>p</sub> [[VAR := E]] = assign-int (L<sub>p</sub> [[VAR]], U<sub>p</sub> [[E]])

assign-int has already been defined in II.1.1.

S<sub>p</sub> [[if E1 eq E2 then SL1 else SL2 fi]] =
condit (V<sub>p</sub> [[E1]], V<sub>p</sub> [[E2]], S<sub>p</sub> [[SL1]], S<sub>p</sub> [[SL2]])

S<sub>p</sub> [[call ID (E, VAR)]] =
proc-call (proc-id 'ID', V<sub>p</sub> [[E]], L<sub>p</sub> [[VAR]], proc-id 'P')

The definition of *proc-call* is the concatenation of three modifications. The
first one is a concurrent substitution which describes :

- the modification of the calls chain

- the assignments of parameters.

The second one is the body of the procedure. The last one specifies the return.

(proc-id, int, var, proc-id) → modif : proc-call ;

proc-call (p-id, i, v, p) =
concat ( subst (<caller (current call), name (current call),
value of ( appoints ( param1 (p-id), current call))),
refers to ( ref-appoints (param2 (p-id), current call))),
<current call, p-id, i, v>),
concat ( possesses (p-id), subst (current call, caller (current call))))

There is a restriction on the use of the modification *proc-call* :

Pre (proc-call ; p-id, i, v, p) =
ANCESTOR (p-id, p) v (father (p-id) = p) v (father (p-id) = father (p))
This precondition reflects the scope rules for procedure calls.
Note that substitution embodies a very powerful means to specify the
creation of a new call and of the new variables associated with it : in
every valid formula the occurrences of current call are replaced by
caller (current call), and from the axioms about caller and appoints one
can see that the "new" current call is different from all the other calls
and that the variables local to the called procedure are different from all
the other variables.

Let us get now to the semantic functions V and L.

V is defined by :

$$
V_p [\text{INT}] = \text{int 'INT'}
$$

$$
V_p [\text{VAR}] = \text{value of } (L_p [\text{VAR}])
$$

$$
V_p [E+T] = \text{plus} (V_p [E], V_p [T])
$$

and similarly for sub, mult and div.

For L, we can write :

$$
L_p [\text{ID}] = \underset{\text{then appoints (var-id 'ID', current call)}}{\text{if}} ID \in \text{var-id} \wedge \text{ANCESTOR (father (var-id 'ID'), proc-id 'P')}
$$

$$
\text{elseif } ID \in \text{ref-id} \wedge \\
\qquad \text{ANCESTOR (father (ref-id 'ID'), proc-id 'P'))} \\
\qquad \text{then refers to (ref-appoints (ref-id 'ID', current call))}
$$

$$
L_p [\text{ID[E]}] = \underset{\text{then element (array 'ID', current call, } V_p [\text{E}]\text{)}}{\text{if}} ID \in \text{array-id} \wedge \text{ANCESTOR (father (array-id 'ID'), proc-id 'P')}
$$

$$
\text{then element (array 'ID', current call, } V_p [\text{E}] \text{)}
$$

II.2.3 Example

In order to improve the reader's intuitive understanding, we give here an
example of the formula associated with a program. In this program, the proce-
dure P exchanges the values of A[I] and X; A is a global variable with respect
to P, and I and X are its formal parameters, passed respectively by value and
as a variable.

The call 'call P(A[1], A[1])' is then used to exchange A[A[1]] and A[1],
i.e. A[2] and A[1].
```
array A[2];
proc P (val I, var X)
    begin
        integer INT;
        INT := X;
        X := A[I];
        A[I] := INT
    end;
    A[1] := 2;
    A[2] := 1;
    call P (A[1], A[1])
```

We are not going to write the full formula, but instead we shall give
the meaning of the declarations of A and P, and that of the call of P.

The semantic value of the first line is given by :

$$S_{\text{PROG}} [[\text{array A}[2]]] = \text{decl-array (array-id 'A', int '2', proc-id 'PROG')}$$

To the body of the procedure P is associated the formula :

```
concat (
    decl-int (var-id 'INT', proc-id 'P'),
    concat (
        concat (
            assign-int (
                appoints (var-id 'INT', current call),
                value of (ref-appoints (ref-id 'X', current call))),
            assign-int (
                ref-appoints (ref-id 'X', current call),
                value of (
                    element (
                        array-id 'A',
                        current call,
                        value of (var-id 'I', current call)))))
        ),
        assign-int (element (array-id 'A',
                             current-call,
                             value of (var-id 'I', current call)),
                    value of (var-id 'INT', current call))))
)
```
Let us denote this formula by $B_p$ (body of P). We then have, for the
whole declaration of the procedure P, the following formula :

decl-proc (proc-id 'P', var-id 'I', ref-id 'X', proc-id 'PROG', B_p)

We come at last to the call of P. Its meaning is straightforward to
obtain from the definition of S :

$S_{PROG} [[call P(A[1], A[1])] =$

proc-call (
proc-id 'P'
value of (element (array-id 'A', current call, int '1')),
element (array-id 'A', current call, int '1'),
proc-id 'PROG')
## CONCLUSION

The aim of this paper was to give an idea of the formalism we use to product and prove compilers. We needed to extend the notion of algebraic data type in order to take into account what is a change of state. However the syntactic part (types and operations) is very close to the one presented in [Guttag 78] and defines a type algebra where the type of interest is *modif*. The form of the axioms is different since we allow the symbols $\to$ and $\neq$. This is not a major difference because this symbol can be defined using booleans and conditional definitions. The most important point is the introduction of the special primitive operations *appl* and *subst* to specify the semantics of modifications. The main consequence of these extensions is that the method for proving representations is somewhat different from the one presented in [Guttag 76] but no more difficult.

In the system we are currently developing, [Deschamp 76] the semantic functions are specified using semantic attributes [Knuth 68]. Semantic attributes are also used to compute (or to keep the result of) the operations which describe "static" relations, i.e. operations whose result is available at compile-time : for instance *father* or *name (current call)*. In the description of SIMPROC we just gave, this last function is computed as the first variable of the semantic functions : in fact this variable is an inherited attribute.

At this time, we consider that the main advantage of this formalism is that it is a useful tool to specify, produce and prove compilers. But there are certainly many other interesting applications such as code optimization etc.

## ACKNOWLEDGMENTS

We are deeply indebted to Professor C. PAIR for his help in this research especially in simplifying the abstract data type. Thanks are due to S. SCHUMAN for his improvements of the text.
BIBLIOGRAPHY

[Apt 77] K.R. APT, J.W. DE BAKKER, Semantics and Proof Theory of Pascal Procedures, Report IW 80/77, Mathematisch Centrum, Amsterdam.

[Courcelle 78] B. COURCELLE, M. NIVAT, The Algebraic Semantics of Recursive Program Schemes, Rapport Laboria n° 300, May 1978.

[Deschamp 78] Ph. DESCHAMP, M. MAZAUD, Application des Structures de Données d'un Langage Source à la Spécification d'un Compilateur - (PHASE1). Manuel d'Utilisation - IRIA, June 1978.

[Deschamp 79] Ph. DESCHAMP, Sémantique du passage des procédures en paramètre, Rapport Laboria (to appear).

[Gaudel 77] M.C. GAUDEL, A Formal Approach to Translator Specification, Information Processing 77, B. Gilchrist (Ed), IFIP, North Holland 1977.

[Gaudel 79a] Thesis (to appear).

[Gaudel 79b] M.C. GAUDEL, C. PAIR, Algebraic Data Types as Models of Information Structure, Rapport Laboria (to appear).

[Goguen 77] J. GOGUEN, Abstract Errors for Abstract Data Type, Working Conference on Formal Description of Programming Concepts, ST Andrew, August 1977.

[Guttag 76] J.V. GUTTAG, E. HOROWITZ, D.R. MUSSER, Abstract Data Types and Software Validation, Report ISI/RR-76-48 August 1976.

[Guttag 78] J.V. GUTTAG, J.H. HORNING, The Algebraic Specification of Abstract Data Types, Acta Informatica 10, 27-52 1978.

[Guttag 78b] J.V. GUTTAG, Notes on Type Abstraction, NATO International Summer School, München, August 1978.

[Knuth 68] D.E. KNUTH, Semantics of Context-free Languages, Mathematical Systems Theory, Vol. 2, n° 2, 1968.

[Remy 74] J.L. REMY, Structures d'Information - Formalisation des notions d'accès et de modifications d'une donnée - Thèse de 3ème cycle. Université de Nancy Juin 1974.

[Tennent 76] R. TENNENT, The Denotational Semantics of Programming Languages, CACM, Vol 19, n° 8 August 1976.