# A complete machine-checked definition of a simple programming language using denotational semantics

Veronique Viguie Donzeau-Gouge, Bernard Lang, Gilles Kahn

► To cite this version:

Veronique Viguie Donzeau-Gouge, Bernard Lang, Gilles Kahn. A complete machine-checked definition of a simple programming language using denotational semantics. [Research Report] IRIA-RR-330, IRIA. 1978, pp.33. hal-04716568

HAL Id: hal-04716568

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

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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

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

INV 05447

ARCHIVES

laboratoire de recherche
en informatique
et automatique

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

ARCHIVES

A COMPLETE
MACHINE-CHECKED DEFINITION
OF A SIMPLE
PROGRAMMING LANGUAGE
USING
DENOTATIONAL SEMANTICS

Véronique DONZEAU-GOUGE

Gilles KAHN
Bernard LANG

Rapport de Recherche N° 330

Octobre 1978
# A COMPLETE MACHINE-CHECKED DEFINITION OF A SIMPLE PROGRAMMING LANGUAGE USING DENOTATIONAL SEMANTICS

## Véronique Donzeau-Gouge, Gilles Kahn, Bernard Lang

### Résumé :

Ce rapport discute l'organisation d'une définition formelle complète, en sémantique dénotationnelle, d'un langage de programmation. Le langage ASPLE, utilisé plusieurs fois déjà dans la littérature, sert d'exemple. La définition formelle d'ASPLE a été utilisée comme donnée pour le système SIS de Peter Mosses, permettant ainsi de vérifier la cohérence des programmes et de les exécuter.

### Abstract :

This report discusses the organization of a complete formal definition in denotational semantics. The language ASPLE, taken from the literature is used as an example. The formal definition of ASPLE has been used as an input to Mosses'SIS system. Programs in ASPLE have been satisfactorily typechecked and run.
# INTRODUCTION

Several methods of formal definition of programming languages were surveyed in [1]. Most notably missing from this survey was a presentation of denotational semantics, the method pioneered by Strachey [2,3,4]. To fill this gap, we give here a formal definition of ASPLE, the example programming language used throughout the survey, using denotational semantics.

This report presents two further points of interest. First, it makes use of the idea of non-standard interpretation [5,6,7] : the semantics are not defined on programs but on typechecked programs. The typechecker itself is a "non-standard" semantic function.

It performs all so-called compile-time typechecking and produces a program where all coercions have been made explicit and all type information needed at run-time is available locally. A pretty-printer is also given as a semantic function from programs to strings.

Secondly, this complete formal definition of ASPLE is in machine readable form. It has been fairly extensively tested using Mosses's system SIS [8]. ASPLE programs were satisfactorily run using solely the formal definition as an input to SIS. In that respect, the formal definition given here seems significantly more trustworthy than the four alternate definitions given in [1].

This report is divided into five parts :

1. Specification of the concrete and abstract syntax of ASPLE

2. Presentation of the idea of non-standard denotation :
specification of a pretty-printer for ASPLE programs

3. Definition of a type-checker for ASPLE as another non-standard denotation

4. Formal semantics of ASPLE.

5. Examples and discussion.
# I. CONCRETE AND ABSTRACT SYNTAX OF ASPLE

The syntax of a programming language is given by rules that define a set of strings. On the other hand, the semantics is defined on the abstract syntax of the language, i.e. it maps trees to denotations. Hence it is necessary to specify the correspondence between concrete strings and abstract syntax trees. The purpose of table I is to specify simultaneously the concrete and abstract syntax of ASPLE. It is not necessary here to explain all the details of the notation devised by Mosses for this purpose. The reader is referred to [8]. We insist here only on a few design decisions in the abstract syntax of ASPLE.

1. All indications of precedence, such as the use of parenthesis, vanish in the abstract syntax.

2. All lists of syntactic constituents will be represented as lists of subtrees. This is somewhat at odds with the custom in denotational semantics, but follows the philosophy of MENTOR [9].

3. To stay closer to the syntactic specification of ASPLE in [1] we create distinct nodes for each operator (such as +, -, =, ≠) and also distinct nodes for "if-then-fi" and "if-then-else-fi". This will make the semantics slightly more cumbersome than need be, but simplifies the abstract syntax specification.

4. Lexical items (such as identifiers, numerical or boolean constants) are "tagged" with their type. Hence most semantic functions will not need to know the internal representation of these items. ;

The lexical part of the specification of ASPLE does not require any particular comment.
<caption>TABLE I</caption>

GRAM "ASPLE"
!**********************************************************************
SYNTAX
!**********************************************************************
program ::= "begin" dcl-train STM-train "end" ;

! [Declarations]
!-----------
dcl-train ::= declaration+ ;

declaration ::= mode idlist ";" ;

mode ::= "bool" : "bool" /
"int" : "int" /
"ref" mode ;

idlist ::= id+-"," ;

! [Statements]
!-----------
stm-train ::= statement+-";" ;

statement ::= asgt-stm :asgt-stm /
               cond-stm :cond-stm /
               loop-stm :loop-stm /
               transput-stm :transput-stm ;

asgt-stm ::= id ":=" exp ;

cond-stm ::= "if" exp "then" STM-train "fi" /
             "if" exp "then" STM-train "else" STM-train "fi" ;

loop-stm ::= "while" exp "do" STM-train "end" ;

transput-stm ::= "input" id /
                 "output" exp ;

! [Expressions]
!-----------
exp ::= factor:factor /
      exp "+" factor ;

factor ::= primary:primary /
            factor "*" primary ;

primary ::= id : id /
             constant : constant /
             "(" exp ")" : exp /
             "(" compare ")" : compare ;

compare ::= exp "=" exp /
             exp "#" exp ;
! [Constants and Identifiers]
!---------------------------------

id ::= ident ;

constant ::= bool /
             num ;

bool ::= "true" : TT /
        "false" : FF ;

num ::= "NUM" n : n ;

ident ::= "ID" q : q ;

**********

DOMAINS !*

**********

dcl-train,declaration: Dcl;

stm-train,statement: Stm ;

exp,factor,primary,compare : Exp;

**************************************************

LEXIS

!*

**************************************************

program ::= word+ : (CONC word+ ) ;

word ::= layoutchar+ : <>
        identifier : <OUT "ID", identifier > /
        numeral : <OUT "NUM",numeral > ;

layoutchar === " "/ CC"C" / CC"L" ;

identifier ::= letter+ : (QUOTE letter+ ) ;

letter ::= "A"..."Z" ;

numeral ::= digit+ : (NUMBER digit+) ;

digit ::= "0"..."9" ;

END
## II. PRETTY-PRINTING ASPLE PROGRAMS

Denotations of programs usually take their values in some elaborate function space. Other kinds of less abstract denotations may also be very useful. As an example, we show on table 2 a string denotation. The semantic function "pretty" maps an abstract syntax tree into a string of characters. In defining this function, our primary concern was simplicity. Currification and continuations are not mandatory here so they are not used. Similarly, the pretty-printer is not very sophisticated : it assumes an unbounded line length and doesn't compute pages. On the other hand, it is easy to figure out how to incorporate these features, once the flavor of the definition is understood. The careful reader will note that "pretty" is defined over an extended abstract syntax. This is because it can be used to pretty-print not only programs but "typechecked" programs as well.

### Remarks :

- The pretty-printer does a small amount of normalization over arithmetic expressions since parentheses are restored only when they are needed due to the relative precedence of operators.

- The correctness of the pretty-printer is to be specified in terms of its relation to the semantics of programs : for example the way in which programs are indented should reflect the scope structure of the language. Proofs of such facts (say in LCF [10]) should be easier since pretty-printer and semantics are expressed in the same formalism.
<caption>TABLE II</caption>

DSL "ASPLE pretty-print"

**DOMAINS**

! SYNTACTIC DOMAINS
! ******************

prog : Prog = ["begin" Dcl Stm "end"] ;
dcl : Dcl = [ Dcl+ ]
           / [ Mode Idlist ";"]
           ;
mode : Mode = "bool" / "int" / ["ref" Mode] ;
idlist : Idlist = [ Id+ ] ;
stm : Stm = [ Stm+ ]
           / [ Id ":=" Exp ]
           / ["if" Exp "then" Stm "fi"]
           / ["if" Exp "then" Stm "else" Stm "fi"]
           / ["while" Exp "do" Stm "end"]
           / ["input" Id ]
           / ["output" Exp ]
           / ["output" Exp Mode ]
           / ["input" Exp Mode ]
           ;
exp : Exp = [ Exp "+" Exp ]
           / [ Exp "*" Exp ]
           / [ Exp "=" Exp ]
           / [ Exp "#" Exp ]
           / ["deref" Exp ]
           / [ Exp "or" Exp ]
           / [ Exp "and" Exp ]
           / Id
           / [Num]
           / [Bool]
           ;
id : Id = [Ident] ;
ident : Ident = Q ;
num : Num = N ;
bool : Bool = T ;

! TYPE DECLARATIONS
! ******************

! [Variables]
!-------------
tree : Tree = P ;
q,margin,new-margin,separ,crlf : String = Q ;
stringlist : Stringlist = Q* ;
! [Functions]
!-------------
pretty := Tree -> String ;
unparse := <Tree,String> -> String ;
unparlist := <Tree,String,String> -> String* ;
simplestm := Tree -> T ;
! FUNCTIONS DEFINITIONS

! ****************************

LET crlf = QUOTE<CC"C",CC"L">

DEF pretty(tree):String = QUOTE <crlf,unparse(tree,crlf),crlf>
WITH
  unparse(tree,margin):String =
    LET new-margin = QUOTE<margin,"
    LET stringlist =
      CASE tree
        !Program
        !******
        /["begin" dcl STM "end"] ->
          <"begin",
            new-margin,unparse(dcl,new-margin),
            new-margin,unparse(stm,new-margin),
            margin,"end">
        !Declarations
        !********
        /[dcl+] ->
          unparlist(dcl+,margin,margin)
        /[mode idlist ";"] ->
          <unparse mode,margin)," ",
          unparse(idlist,margin),";">
        /["ref" mode] ->
          <"ref ",unparse mode,margin">
        /"int" -> <"int">
        /"bool" -> <"bool">
        /[id+] ->
          unparlist(id+,margin,",")
        !Statements
        !********
        /[stm+] ->
          unparlist(stm+,margin,QUOTE<";",margin>)
        /[id ":=" exp] ->
          <unparse(id,margin)," := ",unparse(exp,margin)>
        /["if" exp "then" STM "fi"] ->
          <"if ",unparse(exp,margin)," then ",
            (simplestm(stm) ->
              QUOTE <unparse(stm,margin)," ">,
              QUOTE <new-margin,unparse(stm,new-margin),margin>),
            "fi">
        /["if" exp "then" STML "else" STM2 "fi"] ->
          <"if ",unparse(exp,margin)," then",
            new-margin,unparse(stml,new-margin),
            margin,"else",
            new-margin,unparse(stm2,new-margin),
            margin,"fi">
        /"while" exp "do" STM "end"] ->
          <"while ",unparse(exp,margin)," do",
            new-margin,unparse(stm,new-margin),
            margin,"end">
        /["input" id] ->
          <"input ",unparse(id,margin)>
        /["input" exp mode] ->
          <"input ",unparse(exp,margin)," [",unparse mode,margin),"]">
        /["output" exp] ->
          <"output ",unparse(exp,margin)>
        /["output" exp mode] ->
          <"output ",unparse(exp,margin)," [",unparse mode,margin),"]>
### Expressions

**[expressions]**

```
/[expr "+" exp2] ->
    <unparse(expl,margin)," + ",unparse(exp2,margin)>

/[expr "or" exp2] ->
    <unparse(expl,margin)," or ",unparse(exp2,margin)>

/[expr "*" exp2] ->
    <unparse'(expl,margin)," * ",unparse'(exp2,margin)>

/[expr "and" exp2] ->
    <unparse'(expl,margin)," and ",unparse'(exp2,margin)>

/[expr "=" exp2] ->
    <"(" ,unparse(expl,margin)," = ",unparse(exp2,margin),")">

/[expr "#" exp2] ->
    <"(" ,unparse(expl,margin)," # ",unparse(exp2,margin),")">

/["deref" exp] ->
    <"deref ",unparse(exp,margin)>
```

### Constants and Identifiers

**[constants and identifiers]**

```
/[ident] -> <ident>
/[num] -> LET NUMBER q+ = num IN q+
/[bool] -> bool -> <"true">,<"false">
/? -> <"??">
```

### ESAC

**IN QUOTE stringlist**

**WITH**

```
unparlist(tree,margin,separ):Stringlist =
    CASE tree
        /(treel PRE tree2+) ->
            <unparse(treel,margin),
            separ,
            QUOTE unparlist(tree2+,margin,separ)>
        /<treel> ->
            <unparse(treel,margin)>
```

### ESAC

**WITH**

```
simplestm(tree):Tree =
    CASE tree
        /[id ":=" exp]
        /"input" id
        /"input" exp mode
        /"output" exp] -> TT
        /[stm+] -> simplestm(stm+)
        /<treel> -> simplestm(treel)
        /? -> FF
```

### ESAC

**IN**

```
pretty : (Tree -> String)
END
```
# III. TYPE CHECKING ASPLE PROGRAMS

## a) General remarks

The concept of non-standard interpretation was first proposed, in the GIER Algol Compiler, to perform type-checking [5]. The type checker presented here is a mapping from abstract syntax trees to extended abstract syntax trees, parametrized by the "machine context" for which this type checking is to be accomplished. Typechecked programs contain no implicit coercions, and all type information needed at run time (i.e. for transput operations) is available locally. Therefore, the formal semantics will not need static environments. This organisation seems to mimic rather well the concepts of "compile time" checks and "run-time" checks. Table 3 contains the definition of the type checking function check-prog.

In fact, a type-checker incorporates three distinct functions that could be embodied in distinct passes :

- First, one must check that all identifiers are declared, and that there are no repeated declarations of the same identifier within the same scope.

- Second, one must check that all identifiers are used in a manner that is consistent with the type they have been assigned.

- Third, all information on types of identifiers must be used to generate an extended abstract syntax tree. The decision made here to have a unique pass which perform these three functions follows conventional wisdom but may not be the best in general.

## b) Context

The type-checker is parametrized by a "machine context". Here, the machine context is a single integer, the maximum integer available on the machine for which programs are being type-checked. This information is needed by the type-checker to track down illegal manifest constants. In general, the "machine context" would also contain information on the restrictions of the compiler as well. Of course, this same context will be a parameter of the standard semantics since it specifies when overflow, for example, will occur.
### c) Environments and consistency checks

ASPLE has a flavour of Algol 68. All expressions possess modes that are either basic modes (i.e. `int`, `bool`) or reference-to a mode. Checking declarations consists in building an environment of type :

Ident → Den

where any denotation in `Den` is either a mode (correct declaration) or "err" (double-declaration) or undefined (no declaration). We have followed as closely as possible the informal introduction to ASPLE given in [1] so that when `A` is declared

int `A`;

the identifier `A` is entered in the environment with denotation reference-to-integer. Similarly, when checking assignment statements, we follow literally the description of [1]. As a consequence, the semantics will not need to distinguish between left-values and right-values of expressions.

Example : the assignment
`A := A + 1` is understood as meaning
`A := deref A + 1`

Note the strange rules of ASPLE with respect to boolean values :
they may be added (i.e. `OR ed`) or multiplied (i.e. `AND ed`) but not com-
pared for equality of inequality !

### d) Construction of the result and treatment of errors

First of all, the abstract syntax is enriched with :

- a "deref" operator for explicit dereferencing

- "or" and "and" operators, used after "+" and "*"
have been disambiguated

- binary transput statements that are meant to contain
the base-type information, needed at run time to
check the validity of input or to "format" output

The type-checker then proceeds by reconstructing the tree it
is analyzing, inserting here and there new operators. In case of an
error, it puts an undefined value as a resulting subtree at the lowest
meaningful level. This mechanism provides a simple form of error recovery.
The type-checker could give up entirely instead, or record an error message
in the tree. All solutions are equally feasible and we made an intermediate
choice. The last solution is probably best in the long run, since it
also provides a standard for error messages.
<caption>TABLE III</caption>

DSL "ASPLE type-check"
DOMAINS

! SYNTACTIC VARIABLES AND DOMAINS
! ****************************
prog : Prog = ["begin" Dcl Stm "end"] ;
dcl : Dcl = [ Dcl+ ]
             / [ Mode Idlist ";"]
             ;
mode : Mode = "bool" / "int" / ["ref" Mode] ;
idlist : Idlist = [ Id+ ] ;
stm : Stm = [ Stm+ ]
             / [ Id ":=" Exp ]
             / ["if" Exp "then" Stm "fi"]
             / ["if" Exp "then" Stm "else" Stm "fi"]
             / ["while" Exp "do" Stm "end"]
             / ["input" Id ]
             / ["output" Exp ]
             / ["output" Exp Mode ]
             / ["input" Exp Mode ]
             ;
exp : Exp = [ Exp "+" Exp ]
             / [ Exp "*" Exp ]
             / [ Exp "=" Exp ]
             / [ Exp "#" Exp ]
             / [ Exp "or" Exp ]
             / [ Exp "and" Exp ]
             / ["deref" Exp ]
             / Id
             / [Num]
             / [Bool]
             ;
id : Id = [Ident];
ident: Ident = Q ;
num : Num = N ;
bool : Bool = T ;

SEMANTIC VARIABLES AND DOMAINS
!***************************
d : Den = Mode / "err" ;
e, initial-env : Env = Ident -> Den ;

!TYPES OF SEMANTIC FUNCTIONS
!***************************
check-dcl  := <Dcl,Env> -> <Dcl,Env>;
check-id  := <Id,Env,Mode> -> <Id,Env>;
check-exp := <Exp,Env> -> <Exp,Den> ;
check-prog := Prog -> Prog ;
check-stm := <Stm,Env> -> Stm ;
check-stm-list := <Stm*,Env> -> Stm* ;
check-dcl-list := <Dcl*,Env> -> <Dcl*,Env> ;
check-id-list := <Id*,Env,Mode> -> <Id*,Env> ;
base-level := Den -> <Den,N>;
deref := <Exp,N> -> Exp ;
WITH
!EXPRESSIONS
!**********

check-exp (exp,e):<Exp,Den> =
  CASE exp
    /* ... */
  /[ident] ->
    LET d = e ident
    IN (d EQ "err") OR (d EQ?) !Ill- or un-declared
      -> <?,"err">,
          <[ident], d>
    /[num] -> ( num LE maxint -> <[num],"int">,<?,"err">)
    /[bool] -> <[bool],"bool">
    /* ... */
  /[exp1 "+" exp2] ->
    LET <exp1,d1> = check-exp (exp1,e)
    ALSO <exp2,d2> = check-exp (exp2,e)
    LET <d'1,n1> = base-level (d1)
    ALSO <d'2,n2> = base-level (d2)
    IN
      (d'1 EQ d'2) AND (d'1 NE "err") ->
        (LET exp'1 = deref (exp1,n1)
           ALSO exp'2 = deref (exp2,n2)
           IN (d'1 EQ "int") ->
              <[exp'1 "+" exp'2],d'1>,
              <[exp'1 "or" exp'2],d'1>),
              <?,"err">)
    /* ... */
  /[exp1 "*" exp2] ->
    LET <exp1,d1> = check-exp (exp1,e)
    ALSO <exp2,d2> = check-exp (exp2,e)
    LET <d'1,n1> = base-level (d1)
    ALSO <d'2,n2> = base-level (d2)
    IN
      (d'1 EQ d'2) AND (d'1 NE "err") ->
        (LET exp'1 = deref (exp1,n1)
           ALSO exp'2 = deref (exp2,n2)
           IN (d'1 EQ "int") ->
              <[exp'1 "*" exp'2],d'1>,
              <[exp'1 "and" exp'2],d'1>),
              <?,"err">)
/*[expl "=" exp2] ->
    LET <exp1,d1> =check-exp(exp1,e)
    ALSO <exp2,d2> =check-exp(exp2,e)
    LET <d'1,n1> = base-level(d1)
    ALSO <d'2,n2> = base-level(d2)
  IN
  (d'1 EQ "int") AND (d'2 EQ "int") ->
    (LET exp'1=deref(exp1,n1)
       ALSO exp'2=deref(exp2,n2)
    IN <[exp'1 "=" exp'2],"bool">),
    <?,"err">)

/*[expl "#" exp2] ->
    LET <exp1,d1> =check-exp(exp1,e)
    ALSO <exp2,d2> =check-exp(exp2,e)
    LET <d'1,n1> = base-level(d1)
    ALSO <d'2,n2> = base-level(d2)
  IN
  (d'1 EQ "int") AND (d'2 EQ "int") ->
    (LET exp'1=deref(exp1,n1)
       ALSO exp'2=deref(exp2,n2)
    IN <[exp'1 "#" exp'2],"bool">),
    <?,"err">)

ESAC

WITH
  !auxiliary functions for checking expressions
  !--------------------------------------
  base-level (d) :<Den,N> =
    CASE d
      /"ref" mode] -> LET <d',n'> = base-level mode
        IN <d',n' PLUS 1>
      /"int"/"bool"/"err" -> <d,0>
      / ? -> <"err",0>
    ESAC

WITH
  deref (exp,n) :Exp =
    n EQ 0 -> exp, deref(["deref" exp], n MINUS 1)
WITH
!STATEMENTS
!********

check-stm (stm,e) : Stm =

    CASE STM
    /[stm+] -> LET STM' = check-stm-list(STM+,e)
           IN [STM']

    /"if" exp "then" STML "fi"] ->
        LET <exp',d> = check-exp (exp,e)
        LET <d',n> = base-level(d)
        LET exp' = (d' EQ "bool" -> deref(exp',n), ?)
        ALSO STM' = check-stm(STML,e)
        IN
        ["if" exp' "then" STM' "fi"]

    /"if" exp "then" STML "else" STM2 "fi"] ->
        LET <exp',d> = check-exp(exp,e)
        LET <d',n> = base-level(d)
        LET exp' = (d' EQ "bool" -> deref(exp',n), ?)
        ALSO STML' = check-stm(STML,e)
        ALSO STM2' = check-stm(STM2,e)
        IN
        ["if" exp' "then" STML' "else" STM2' "fi"]

    /"while" exp "do" STM "end"] ->
        LET <exp',d> = check-exp(exp,e)
        LET <d',n> = base-level(d)
        LET exp' = (d' EQ "bool" -> deref(exp',n), ?)
        ALSO STM' = check-stm(STM,e)
        IN
        ["while" exp' "do" STM' "end"]

    /"input" id] ->
        LET <id,d> = check-exp(id,e)
        LET <mode,exp> =
            (d EQ "err") -> <?,?>,
            LET <d',n> = base-level(d)
            IN <d',deref(id,n MINUS 1)>
        IN ["input" exp mode]
```pascal
/["output" exp] ->
  LET <exp',d> = check-exp(exp,e)
  LET <mode,exp''> =
    d EQ "err" -> <?,?>,
    LET <d',n>=base-level(d)
    IN <d',deref(exp',n)>
  IN ["output" exp' mode]
```

```pascal
/[id ":=" exp] ->
  LET <id1,d1> = check-exp(id,e)
  ALSO <exp1,d2> = check-exp(exp,e)
  LET <d'1,n1> = base-level(d1)
  ALSO <d'2,n2> = base-level(d2)
  IN
    (d'1 EQ d'2) AND (d'1 NE "err") ->
      ( (n1 LE (n2 PLUS 1)) ->
        LET n'=(n2 PLUS 1) MINUS n1
        LET exp'1 = deref(expl,n')
        IN [id1 ":=" exp'1] ,
           ? ),
      ? ),
```

ESAC

```pascal
WITH
  !Auxiliary function for checking statements
  !--------------------------------------------------
  check-stm-list(stm*,e): Stm* =
    CASE stm*
      / stml PRE STM2* ->
        (check-stm(stml,e) PRE
          check-stm-list(stm2*,e) )
      / <> -> < >
    ESAC
```

```pascal
IN
  check-prog(prog):Prog
END
```
# IV. FORMAL SEMANTICS OF ASPLE

## a) Introduction

The "real" formal semantics of ASPLE is now presented. It has been structured, following suggestions of P. Mosses, into three parts :

- An abstract-machine, that provides a possible model of storage allocation and transput operations.

- A "concrete" machine, that specifies what kind of restrictions may occur at run-time.

- A function "semant", parametrized by the machines above.

## b) The function semant

This function is defined on table 4. Syntactic and semantic domain definitions are self explanatory. Note that no information is given on the structure of states. It is left to the abstract machine to propose a possible model of the state. Continuations are mandatory to take in account various run time errors :

- Accessing uninitialized variable

- Overflow

- End of file

- Incorrect input

### b.1) - Declarations

Declaration elaboration is rather simple since the program is supposed to be type-checked. The only work performed at this stage is storage allocation for variables. Much of this could be delegated to the abstract machine, that doesn't know the structure of programs, if slightly more work had been performed by the type-checker (i.e. counting the number of refs).

### b.2) - Expressions

Expression evaluation is straight-forward.

### b.3) - Instructions

Instruction execution needs no particular remarks. As is to be expected, the execution of the while statement is described with the help
of a recursively defined continuation exec-cont'. The assignment statement
can be *paraphrased* in English like this :"To execute an assignment id := exp
in an environment env, with a continuation exec-cont :

- First evaluate the left-hand side identifier in env, returning a location loc.

- Then evaluate the right-hand side expression in the same environment, returning a value.

- Then update the location loc with this value.

- And carry-on executing exec-cont."

This paraphrasing is slightly misleading, since it makes
continuation handling appear quite magical, but it helps reading dry
equations. Running a program (function "run") can be explained in a similar
fashion :

"- First elaborate its declarations in the empty environment,
  returning a new environment env.

- Then execute the body of the program in that environment.

- And terminate."

c) Abstract machine

This machine is defined on table 5. It models the state as
a pair <m, last> where

- m is a function from locations to values

- last is the index of the last location in use.

Locations are integer values and allocating storage is
straight-forward. When accessing a location that has never been assigned
an error occurs.

Input and output are simple but slightly asymmetrical LAMB
constants are read in because we didn't want to include here a lexical
scanner (it should be done for completeness) and strings of characters
are output (Note that ASPLE doesn't tell you what to do at the end of a line).

d) Concrete machine

This is only the maximum integer available on the machine.
<caption>TABLE IV</caption>

DSL "ASPLE semantics"
DOMAINS

! SYNTACTIC VARIABLES AND DOMAINS

! ****************************

prog : Prog = ["begin" Dcl Stm "end"] ;
dcl : Dcl = [ Dcl+ ]
         / [ Mode Idlist ";"]
         ;
mode : Mode = "bool" / "int" / ["ref" Mode ] ;
idlist : Idlist = [ Id+ ] ;
stm : Stm = [ Stm+ ]
        / [ Id ":=" Exp ]
        / ["if" Exp "then" Stm "fi"]
        / ["if" Exp "then" Stm "else" Stm "fi"]
        / ["while" Exp "do" Stm "end"]
        / ["input" Id ]
        / ["output" Exp ]
        / ["output" Exp Mode ]
        / ["input" Exp Mode ]
        ;
exp : Exp = [ Exp "+" Exp ]
         / [ Exp "*" Exp ]
         / [ Exp "=" Exp ]
         / [ Exp "#" Exp ]
         / [ Exp "or" Exp ]
         / [ Exp "and" Exp ]
         / ["deref" Exp ]
         / Id
         / [Num]
         / [Bool]
         ;
id : Id = [Ident] ;
ident: Ident = Q ;
num : Num = N ;
bool : Bool = T ;

!SEMANTIC VARIABLES AND DOMAINS

!****************************

<table><tr><td>answ : Answ;</td><td>!Answers</td></tr><tr><td>env : Env = Ident -> Loc;</td><td>!Environments</td></tr><tr><td>exec-cont : Exec-cont = State -> Input* -> Answ;</td><td>!Command continuations</td></tr><tr><td>elab-cont : Elab-cont = Env -> Exec-cont;</td><td>!Declarations continuations</td></tr><tr><td>loc : Loc;</td><td>!Locations</td></tr><tr><td>value : Value = N / T / Loc;</td><td>!Storable value</td></tr><tr><td>eval-cont : Eval-cont = Value -> Exec-cont;</td><td>!Expressions continuations</td></tr><tr><td>state : State;</td><td>!States</td></tr><tr><td>input : Input;</td><td>!Inputs</td></tr></table>
TYPES OF SEMANTIC FUNCTIONS

run := Prog -> Exec-cont;
execute := Stm -> Env -> Exec-cont -> Exec-cont;
execute-list := Stm* -> Env -> Exec-cont -> Exec-cont;
evaluate := Exp -> Env -> Eval-cont -> Exec-cont;
elaborate := Dcl -> Env -> Elab-cont -> Exec-cont;
elaborate-list := Dcl* -> Env -> Elab-cont -> Exec-cont;
elaborate-id := <Id, Mode> -> Env -> Elab-cont -> Exec-cont;
elaborate-id-list := <Id*, Mode> -> Env -> Elab-cont -> Exec-cont;
allocate := <Loc, Mode> -> Exec-cont -> Exec-cont;
no-action := Exec-cont -> Exec-cont;

IN

LAM prog.

PRIMITIVES

**********

LAM <

init-state : State,
wrong : (Q -> Exec-cont),
newloc : (Eval-cont -> Exec-cont),
update : ((Loc,Value) -> Exec-cont -> Exec-cont),
content : (Loc -> Eval-cont -> Exec-cont),
write : ((Value,Mode) -> Exec-cont -> Exec-cont),
read : ((Loc,Mode) -> Exec-cont -> Exec-cont)

>

LAM maxint.

FUNCTIONS DEFINITIONS

LET no-action : (Exec-cont ->Exec-cont ) = LAM exec-cont . exec-cont !Identity on continuations
ALSO init-exec-cont : Exec-cont = LAM state. LAM input*. <> !Initial continuation
ALSO init-env : Env = LAM ident. ? !Empty environment
```pascal
!PROGRAM
!********
```

```pascal
run ["begin" dcl STM "end"] : Exec-cont =
    elaborate(dcl)init-env; LAM env.
    execute(stm)env;
    init-exec-cont
```

WITH

```pascal
!DECLARATIONS
!**********
```

```pascal
elaborate (dcl)env; elab-cont : Exec-cont =
    CASE dcl
        /[dcl+] -> elaborate-list (dcl+)env;
            elab-cont
        /[mode idlist ";"] ->
            LET [id+] = idlist
            IN elaborate-id-list(id+,mode)env;
            elab-cont
    ESAC
```

WITH

```pascal
!Auxiliary functions for declarations
!-----------------------------
```

```pascal
elaborate-list (dcl*)env; elab-cont : Exec-cont=
    CASE dcl*
        /dcl1 PRE dcl2* ->
            elaborate(dcl1)env; LAM env'.
            elaborate-list(dcl2*)env';
            elab-cont
        /<> ->
            LET exec-cont=elab-cont env)
            IN exec-cont
    ESAC
```

WITH

```pascal
elaborate-id-list (id*,mode)env; elab-cont : Exec-cont=
    CASE id*
        /id1 PRE id2* ->
            elaborate-id (id1,mode)env; LAM env'.
            elaborate-id-list (id2*,mode)env';
            elab-cont
        /<> ->
            LET exec-cont=elab-cont env)
            IN exec-cont
    ESAC
```

WITH

```pascal
elaborate-id (id,mode)env; elab-cont : Exec-cont =
    newloc; LAM loc.
    LET [ident] = id
    LET env' = env \ ident<-loc
    LET exec-cont' =! elab-cont (env')
    IN allocate (loc,mode);
    exec-cont'
```

WITH

```pascal
allocate(loc,mode)exec-cont : Exec-cont =
    CASE mode
        /["ref" mode'] -> newloc; LAM loc'.
            update(loc,loc');
            allocate(loc',mode');
            exec-cont
        /"int" /"bool" -> exec-cont !No allocation needed
    ESAC
```
WITH
!STATEMENTS
!********

execute(stm)env;exec-cont : Exec-cont =
    CASE STM
    /[stm+] -> execute-list(stm+)env;
        exec-cont
    [/"if" exp "then" stml "fi"] ->
        evaluate(exp)env; LAM t.
        (t -> execute(stml)env, no-action);
        exec-cont
    [/"if" exp "then" stml "else" STM2 "fi"] ->
        evaluate(exp)env; LAM t.
        (t -> execute(stml)env, execute(stm2)env);
        exec-cont
    [/"while" exp "do" STM "end"] ->
        DEF exec-cont' =
            evaluate(exp)env; LAM t.
            (t -> execute(STM)env;exec-cont', exec-cont)
        IN exec-cont'
    [/"input" exp mode] ->
        evaluate(exp)env; LAM loc.
        read(loc,mode);
        exec-cont
    [/"output" exp mode] ->
        evaluate(exp)env; LAM value.
        write(value,mode);
        exec-cont
    /[id ":=" exp] ->
        evaluate(id)env; LAM loc.
        evaluate(exp)env; LAM value.
        update(loc,value);
        exec-cont

ESAC
WITH
!auxiliary functions for statements
!---------------------------------

execute-list(stm*)env;exec-cont : Exec-cont =
    CASE STM*
    /stml PRE STM2* ->
        execute(stml)env;
        execute-list(stm2*)env;
        exec-cont
    /<> -> exec-cont

ESAC
IN
run (prog) (init-state) : (Input* -> Answer)
WITH
!EXPRESSIONS
**********

evaluate (exp)env; eval-cont : Exec-cont =
  CASE exp
    /* ... */
    /* [ident] -> */
    LET value = env ident
    LET exec-cont = eval-cont (value)
    IN exec-cont
  /* ... */
    /* [num] -> */
    LET exec-cont = eval-cont (num)
    IN exec-cont
  /* ... */
    /* [bool] -> */
    LET exec-cont = eval-cont (bool)
    IN exec-cont
  /* ... */
    /* [exp1 "+" exp2] -> */
    evaluate (exp1) env; LAM value1.
    evaluate (exp2) env; LAM value2.
    LET n = value1 PLUS value2
    IN n LE maxint -> eval-cont (n), wrong "overflow"
  /* ... */
    /* [exp1 "*" exp2] -> */
    evaluate (exp1) env; LAM value1.
    evaluate (exp2) env; LAM value2.
    LET n = value1 MULT value2
    IN n LE maxint -> eval-cont (n), wrong "overflow"
  /* ... */
    /* [exp1 "and" exp2] -> */
    evaluate (exp1) env; LAM value1.
    evaluate (exp2) env; LAM value2.
    LET t = value1 AND value2
    LET exec-cont = eval-cont (t)
    IN exec-cont
  /* ... */
    /* [exp1 "or" exp2] -> */
    evaluate (exp1) env; LAM value1.
    evaluate (exp2) env; LAM value2.
    LET t = value1 OR value2
    LET exec-cont = eval-cont (t)
    IN exec-cont
  /* ... */
    /* [exp1 "#" exp2] -> */
    evaluate (exp1) env; LAM value1.
    evaluate (exp2) env; LAM value2.
    LET exec-cont = value1 NE value2 -> eval-cont (TT), eval-cont (FF)
    IN exec-cont
  /* ... */
    /* [exp1 "=" exp2] -> */
    evaluate (exp1) env; LAM value1.
    evaluate (exp2) env; LAM value2.
    LET exec-cont = value1 EQ value2 -> eval-cont (TT), eval-cont (FF)
    IN exec-cont
  /* ... */
    /* ["deref" expl] -> */
    evaluate (expl) env; LAM loc.
    content (loc);
    eval-cont
  ESAC
<table><caption>TABLE V</caption><thead><tr><th colspan="2">DSL "abstract machine"</th></tr></thead><tbody><tr><td colspan="2"><strong>DOMAINS</strong></td></tr><tr><td colspan="2"><strong>!SEMANTIC VARIABLES AND DOMAINS</strong></td></tr><tr><td colspan="2">!**************************************************</td></tr><tr><td>input</td><td>: Input = N / T;</td></tr><tr><td>answ</td><td>: Answ = Q*;</td></tr><tr><td>mode</td><td>: Mode = "int" / "bool";</td></tr><tr><td>last,loc</td><td>: Loc = N;</td></tr><tr><td>value</td><td>: Value = N / T / Loc;</td></tr><tr><td>m</td><td>: M = Loc -> Value;</td></tr><tr><td>state</td><td>: State = &lt;M,Loc&gt;;</td></tr><tr><td>exec-cont</td><td>: Exec-cont = State -> (Input* -> Answ);</td></tr><tr><td>eval-cont</td><td>: Eval-cont = Value -> Exec-cont;</td></tr><tr><td colspan="2"><strong>!TYPES OF FUNCTIONS</strong></td></tr><tr><td colspan="2">!**************************************************</td></tr><tr><td>init-state</td><td>::= State;</td></tr><tr><td>wrong</td><td>::= Q -> Exec-cont;</td></tr><tr><td>newloc</td><td>::= Eval-cont -> Exec-cont;</td></tr><tr><td>update</td><td>::= &lt;Loc,Value&gt; -> Exec-cont -> Exec-cont;</td></tr><tr><td>content</td><td>::= Loc -> Eval-cont -> Exec-cont;</td></tr><tr><td>write</td><td>::= &lt;Value,Mode&gt; -> Exec-cont -> Exec-cont;</td></tr><tr><td>read</td><td>::= &lt;Loc,Mode&gt; -> Exec-cont -> Exec-cont;</td></tr><tr><td colspan="2"><strong>IN</strong></td></tr><tr><td colspan="2">!DESCRIPTION OF FUNCTIONS</td></tr><tr><td colspan="2">!**************************************************</td></tr><tr><td>LET</td><td>wrong(q)(state)(input*) :Answ = &lt;QUOTE&lt;"ERROR : ",q&gt;&gt;</td></tr><tr><td colspan="2">!State handling</td></tr><tr><td colspan="2">!---------------</td></tr><tr><td>ALSO</td><td>initial-state :State = &lt; LAM loc.? ,0&gt;</td></tr><tr><td>ALSO</td><td>newloc.eval-cont(state) : (Input* -> Answ) =<br/>LET &lt;m last&gt; = state<br/>LET last' = last PLUS 1<br/>LET state' = &lt;m last&gt;<br/>IN eval-cont(last')(state')</td></tr><tr><td>ALSO</td><td>update(loc,value)(exec-cont)(state) : (Input* -> Answ) =<br/>LET &lt;m last&gt; = state<br/>LET m' = m \ loc&lt;-value<br/>LET state' = &lt;m',last&gt;<br/>IN exec-cont(state')</td></tr><tr><td>LET</td><td>content(loc)(eval-cont)(state) : (Input* -> Answ) =<br/>LET &lt;m last&gt; = state<br/>LET value = m(loc)<br/>IN (value NE ?) -> eval-cont(value)(state),<br/>wrong"undefined"(state)</td></tr></tbody></table>
!Input-output

!---------------

ALSO
write(value,mode)(exec-cont)(state)(input*) :Answ =
    LET q = CASE mode
        /"int" ->   LET NUMBER q'* = value
        IN QUOTE q'
        /"bool" ->  (value -> "true", "false")
    ESAC
    IN <q> CAT (exec-cont(state)(input*))

ALSO
read(loc,mode)(exec-cont)(state)(input*) :Answ =
    CASE input*
        /input1 PRE input2* ->
            CASE <input1,mode>
                /<TRUTH ?,"bool"> /<NUMBER ?,"int"> ->
                    update(loc输入1)(exec-cont)(state)(input2*)
                / ? -> wrong"input type"(state)(<>)
            ESAC
        /<> -> wrong"end of file"(state)(<>)
    ESAC

IN <initial-state,wrong,newloc,update,content,write,read>

END

LAMB "concrete-machine"

500

END
## V. EXAMPLES AND DISCUSSION

The formal definition described above has been used as an input to the system SIS. All examples in [1] were satisfactorily treated. On fig. 1 we show the pretty-printer version of the factorial program, in parallel with its typechecked version. Then, one can see that this program ran satisfactorily for the value 3 of its input but overflowed for 6 since $6! = 720$.

On fig. 2 we show a program that doesn't typecheck because a manifest constant is to big. Note that, from the title of the result lambda expression on fig. 1, one can check that the same "concrete-machine" is used for typechecking and running programs. Example 3 on fig. 3 illustrates error recovery in the type-checker.

Example 4 on fig. 4 is a rather obscure program with coercions. It illustrates the Algol-68 feature of ASPLE. Finally, the treatment of a run-time error is displayed on fig. 5. There, an uninitialized variable is being evaluated, causing a message and immediate termination.

## Acknowledgments

We thank Henry Ledgard for suggesting the exercise. Peter Mosses helped us directly and indirectly in using his system SIS, a real jewel. David MacQueen's critical taste in programming was also appreciated.
LAMB "ASPLE pretty-print(ex1)"
"" LAMB "ASPLE pretty-print(ASPLE type-check(ex1)(concrete-machine))"
"begin"
int X,Y,Z;
input X;
Y := 1;
Z := 1;
if (X # 0) then
    while (Z # X) do
        Z := Z + 1;
        Y := Y * Z
end
fi;
output Y
end
"" END

LAMB "data3"
<3>
END

LAMB "ASPLE semantics(ASPLE type-check(ex1)(concrete-machine))(abstract machine)(concrete-machine)
(data3)"

<"6">

END

LAMB "data6"
<6>
END

LAMB "ASPLE semantics(ASPLE type-check(ex1)(concrete-machine))(abstract machine)(concrete-machine)
(data6)"

<"ERROR : overflow">

END
```python
LAMB "ASPLE pretty-print(ex2)"
"
begin
    int X, Y;
    Y := 100;
    X := 600;
    output Y + X
end
"
END

LAMB "ASPLE pretty-print(ASPLE tyPe-check(ex2)(concrete-machine))"
"
begin
    int X, Y;
    Y := 100;
    ???;
    output deref Y + deref X [int]
end
"
END

Figure 2
```

```python
LAMB "ASPLE pretty-print(ex3)"
"
begin
    int A;
    bool B;
    ref int C;
    ref ref int D;
    A := 16;
    A := B;
    C := D;
    C := 20;
    D := A
end
"
END

LAMB "ASPLE pretty-print(ASPLE tyPe-check(ex3)(concrete-machine))"
"
begin
    int A;
    bool B;
    ref int C;
    ref ref int D;
    A := 16;
    ???;
    C := deref deref D;
    ???;
    ???
end
"
END

Figure 3
```
LAMB "ASPLE pretty-print(ex4)"

"

begin

int INTA,INTB;
ref int REFINTA,REFINTB;
ref ref int REFREFINTA,REFREFINTB;
INTA := 100;
INTB := 200;
REFINTA := INTA;
REFINTB := INTB;
REFREFINTA := REFINTA;
REFINTA := INTB;
INTB := REFREFINTA;
input REFREFINTA;
output REFINTB

end

"

END

LAMB "ASPLE pretty-print(ASPLE type-check(ex4)(concrete-machine))"

"

begin

int INTA,INTB;
ref int REFINTA,REFINTB;
ref ref int REFREFINTA,REFREFINTB;
INTA := 100;
INTB := 200;
REFINTA := INTA;
REFINTB := INTB;
REFREFINTA := REFINTA;
REFINTA := INTB;
INTB := deref deref deref REFREFINTA;
input deref deref REFREFINTA [int];
output deref deref REFINTB [int]

end

"

END

LAMB "data"
<300>
END

LAMB "ASPLE semantics(ASPLE type-check(ex4)(concrete-machine))(abstract machine)(concrete-machine)
(data)"

< "300">

END
LAMB "ASPLE pretty-print(ex5)"
"
begin
    int X,Y;
    Y := 3;
    output X;
    output Y
end
"
END

LAMB "ASPLE pretty-print(ASPLE type-check(ex5)(concrete-machine))"
"
begin
    int X,Y;
    Y := 3;
    output deref X [int];
    output deref Y [int]
end
"
END

LAMB "data3"
<3>
END

LAMB "ASPLE semantics(ASPLE type-check(ex5)(concrete-machine))(abstract machine)(concrete-machine)
(data3)"

< "ERROR : undefined">

<caption>Figure 5</caption>
REFERENCES

[1] Marcotty M., Ledgard H.F., Bochmann G.V. : "A Sampler of formal definitions", Computing Surveys, Vol. 8 n° 2 June 1976.

[2] Tennent R.D. : "The denotational semantics of programming languages", CACM Vol 19 n° 8, August 1976.

[3] Stoy J.E. : "Denotational Semantics : The Scott-Strachey approach to programming language theory", MIT Press (1977).

[4] Milne R., Strachey C. : "A theory of programming language semantics", Chapman and Hall (1976).

[5] Naur P. : "Checking of operand types in Algol Compilers", BIT Vol. 5, 1965, 151-163.

[6] Sintzoff M. : "Calculating Properties of Programs by Valuations on Specific Models", ACM Conference on Proving Assertions about Programs, Las Cruces, New-Mexico, January 6-7 1972.

[7] Donzeau-Gouge V. : "Utilisation de la sémantique dénotationelle pour la description d'interprétations non-standard", 3° Colloque International sur la Programmation, Dunod (1978).

[8] Mosses P. : "SIS : a compiler-generator system using denotational semantics", DAIMI, University of Aarhus, 1978.

[9] Donzeau-Gouge V. et al. : "A structure oriented program editor : a first step towards computer assisted programming", International Computing Symposium, North Holland Publishing Co, (1975).