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

ARCHIVES

UTILISATION DE LA
SÉMANTIQUE DÉNOTATIONNELLE
POUR L'ÉTUDE
D'INTERPRÉTATIONS
NON-STANDARD

Véronique DONZEAU-GOUGE

Rapport de Recherche N° 273

Janvier 1978
UTILISATION DE LA SÉMANTIQUE DÉNOTATIONNELLE
POUR L'ÉTUDE D'INTERPRÉTATIONS NON-STANDARD
Véronique Donzeau-Gouge

Résumé :

Des interprétations non-standard d'un programme permettent d'obtenir par un simple calcul des informations sur les résultats et (ou) le comportement du programme. Nous nous intéressons ici à l'interprétation symbolique (définie sur un domaine de termes) et à l'interprétation de validation (définie sur un domaine de propriétés). L'utilisation de la sémantique dénotationnelle pour leur description permet de définir et prouver les relations qui existent entre ces interprétations non-standard et l'interprétation usuelle, dite standard.

Abstract :

Non-standard interpretations can provide information about the results and (or) the computations
of a program. We study here the symbolic interpretation (defined on a domain of terms) and the
validation interpretation (defined on a domain of properties). The use of denotational semantics
allows us to define and prove the validity of the relations between those non-standard interpreta-
tions and the usual one.
## Introduction :

Un programme donné est susceptible d'être interprété de diverses façons. L'interprétation standard permet d'obtenir le résultat du calcul qu'il définit lorsque des valeurs sont données à ses variables libres. Des interprétations non standard (souvent appelées dans la littérature "interprétations abstraites") permettent de calculer certaines propriétées associées à l'interprétation standard du programme en interprétant celui-ci dans un environnement approprié : Sintzoff [7], Wegbreit [10], Cousot [1], utilisent cette technique.

Pour établir ces propriétés des relations doivent exister entre ces diverses interprétations : c'est à l'étude de ces relations que nous allons nous intéresser.

Cette étude nécessite la possibilité de définir, manipuler et comparer des interprétations. Une interprétation peut être définie par une méthode opérationnelle qui utilise les notions de machine abstraite et transition d'états : cette méthode donne une description précise de l'implémentation.

Une interprétation peut également être définie par une méthode dénotationnelle : cette définition fait correspondre aux programmes des entités mathématiques à partir desquelles des preuves peuvent être faites.

Une fonction est associée à chaque construction syntaxique du langage et définit le sens de cette construction dans un modèle mathématique. Notre objectif étant la mise en évidence de relations entre des interprétations, c'est cette dernière méthode que nous allons utiliser.

Nous illustrons cette approche en étudiant deux interprétations non standard :

- *l'interprétation symbolique* : elle correspond à l'interprétation de Herbrand usuelle en logique mathématique. Elle effectue une factorisation des interprétations standard en permettant de déterminer en une seule interprétation les chemins de calcul et leurs résultats.

- *l'interprétation de validation* : elle est définie sur un domaine de propriétés construit suivant le modèle présenté par Wadge et Shamir [6]. Une propriété est un sous ensemble du domaine de base des interprétations standard ; la propriété résultat de cette interprétation lorsque des propriétés $p_i$ sont associées aux variables libres d'un programme, est vérifiée par les résultats de toutes ces interprétations standard qui associent des valeurs satisfaisants $p_i$ aux variables libres de ce programme. Cette interprétation définit une méthode simple de vérification.
# Plan de cette étude

## I - Définition dénotationnelle des interprétations

I.1 Syntaxe abstraite du langage

I.2 Domaines utilisés pour la définition dénotationnelle des interprétations

## II- Définition dénotationnelle de l'interprétation standard

II.1 Domaines

II.2 Fonctions auxiliaires

II.3 Fonctions sémantiques

II.4 Equations

## III- Interprétation symbolique

Définition dénotationnelle de l'interprétation symbolique

III.1 Domaines

III.2 Fonctions auxiliaires

III.3 Fonctions sémantiques

## IV- Relation entre l'interprétation standard et l'interprétation symbolique

IV.1 Relation entre les domaines utilisés dans la dénotation de l'interprétation standard et les domaines utilisés dans la dénotation de l'interprétation symbolique.

IV.2 Propriété

## V - Interprétation de validation

Définition dénotationnelle de l'interprétation de validation

V.1 Domaines

V.2 Fonctions auxiliaires

V.3 Fonctions

V.4 Equations

## VI - Relation entre l'interprétation standard et l'interprétation de validation

VI.1 Relation entre les domaines utilisés par ces deux interprétations

VI.2 Propriété

Conclusion
# I - DEFINITION DENOTATIONNELLE DES INTERPRETATIONS

## I.1 Syntaxe abstraite du langage

Le langage choisi pour illustrer cette approche contient les éléments qui apparaissent couramment dans les langages de programmation et inclut une notion simple de structure de donnée (tableau a une dimension, enregistrement). Nous n'aurons pas à faire son analyse grammaticale ; aussi toutes les complications hors de propos d'un point de vue sémantique, sont supprimées dans la description ci-dessous.

variables : $i ::= i_1, i_2, ..., i_n$

constantes : $n ::= true, false, 0, 1, 2, ..., -1, -2, ...$

déclarations : $\delta ::= i | i:n | i[n_1, ..., n_p] | \delta_1; \delta_2$

Une déclaration peut être :

- une variable i

- une variable initialisée à une constante i:n

- une structure :
  $n_i$ est la constante qui sélecte le $i$-ème élément

Dans le cas d'un tableau les $n_i$ sont des constantes numériques telles que $n_1 < n_2 < ... < n_p$, et sont habituellement désignées par l'intervalle $[n_1...n_p]$

- une suite de déclarations

expressions : $\epsilon ::= i | n | i[\epsilon] | \epsilon_1 \rho \epsilon_2$

opérateurs arithmétiques : $\rho ::= +, -, x, ...$

Une expression peut être :

- une variable

- une constante

- un élément d'une structure

- une opération arithmétique avec comme opérandes des expressions.

expressions booléennes : $\beta ::= \epsilon_1 \tau \epsilon_2 | \beta_1 \mu \beta_2 | true | false$

opérateurs relationnels : $\tau ::= <, >, =, ...$

opérateurs logiques : $\mu ::= v, \wedge, ...$

Une expression booléenne peut être :

- formée à partir d'un opérateur relationnel avec des expressions comme opérandes.

- formée à partir d'un opérateur logique avec des expressions booléennes comme opérandes.

Dans la mesure où nous sommes amenés à introduire le domaine des expressions qui peuvent apparaître en partie gauche d'une affectation, nous définissons :
l-expressions : $\gamma ::= i | i[\epsilon]$

instructions : 
$\gamma ::= null | \lambda \to \epsilon | if \beta then \gamma_1 else \gamma_2 |$
`while` $\beta$ `do` $\gamma$ `| input $(\lambda)$ | output $(\epsilon)$ |
$\gamma_1$; $\gamma_2$

Une instruction peut être

- l'instruction vide : null

- une affectation

- une expression conditionnelle

- une boucle avec condition

- une instruction de lecture et une instruction d'écriture

- une concaténation d'instructions.

Un programme, est une déclaration suivie d'une instruction

$\psi ::= \delta, \gamma$

## 1.2 Domaines utilisés pour la définition dénotationnelle des interprétations

Une fonction est associée à chaque construction du langage et définit son sens. Ces fonctions sont continues et définies sur des domaines. Nous rappelons qu'un domaine est un ordre partiel $<x, \llangle \rangle$ tel que :

a) tout sous ensemble Y de X tel que deux éléments quelconques de Y sont compatibles, admet une borne supérieure.

b) chaque élément de X est une borne supérieure d'éléments finis.

Si $X_1$ et $X_2$ sont des domaines on désigne par :

$X_1 \to X_2$ le domaine des fonctions continues définies sur $X_1$ et à valeur dans $X_2$.

$X_1 \times X_2$ le domaine des couples dont la première composante est un élément de $X_1$ et la deuxième un élément de $X_2$.

$X_1 + X_2$ le domaine $\{(1, x_1) | x_1 \in X_1\} \cup \{(2, x_2) | x_2 \in X_2\} \cup$ avec $\llangle (n,x) \rangle$ et $\ggangle (n',x') \rangle$ ssi $n=n'$ et $x \llangle x' \ggangle$

$X^*$ le domaine $\{\Lambda\} + X + (X \times X) + (X \times X \times X) + \dots$

$X^\omega$ le domaine formé par les séquences finies ou infinies d'éléments de X.

Si $x_1^\omega, x_2^\omega \in X^\omega$ et $x_1^{\omega \llangle x_2^\omega \ggangle}$, si $x_1^\omega$ est une séquence initiale de $x_2^\omega$ et $\forall x^\omega \in X^\omega \Lambda \llangle x^\omega \ggangle$

Pour les démonstrations de ces résultats se reporter à [ 5 ].
## notations

* Si $x \in X_1 \times X_2 \times \dots \times X_m$ et $x = (x_1, x_2, \dots, x_m)$, $x \uparrow i = x_i$

* Si $x \in X_1 + X_2 + \dots + X_m$, $x | X_i = \begin{cases} \text{l'élément } x_i \text{ de } X_i \text{ si } x = (i, x_i) \\ \text{sinon.} \end{cases}$

* Si $x \in X_1 + \dots + X_m$, $x \in X_i = \begin{cases} \text{vrai si } x = (i, x_i) \text{ et } x_i \in X_i \\ \text{faux sinon.} \end{cases}$

* Si $f = \lambda u.v$ nous notons $f[x\downarrow y]$ la fonction $f$ définit par $f' = \lambda u. u = x \rightarrow y, f(u)$

Dans la définition de la syntaxe abstraite du langage nous avons énoncé les domaines syntaxiques du langage : nous les rappelons.

<table><thead><tr><td>Domaines</td><td>meta variables</td></tr></thead><tbody><tr><td>déclarations</td><td>δ</td></tr><tr><td>variables</td><td>i</td></tr><tr><td>constantes</td><td>n</td></tr><tr><td>expressions</td><td>ε</td></tr><tr><td>opérateurs arithmétiques</td><td>ρ</td></tr><tr><td>opérateurs relationnels</td><td>τ</td></tr><tr><td>opérateurs logiques</td><td>μ</td></tr><tr><td>expressions booléennes</td><td>β</td></tr><tr><td>l-expressions</td><td>λ</td></tr><tr><td>instructions</td><td>γ</td></tr><tr><td>programmes</td><td>ψ</td></tr></tbody></table>

Nous allons introduire des continuations (Wadsworth [8]) dans la dénotation de l'interprétation des expressions car des erreurs peuvent apparaître lors de l'accès érroné à un élément d'une structure. Une fonction "erreur" traite les causes anormales d'interruption. Son exécution imprime un message d'erreur et l'exécution du programme n'est pas poursuivie.

Nous n'introduisons pas de continuations dans la dénotation des déclarations et supposons donc que si une erreur intervient pendant l'exécution des déclarations * elle ne perturbe pas l'exécution des instructions du programme.

<footnote>* En particulier si un même identificateur est déclaré plusieurs fois, seule la dernière occurrence de sa déclaration est utilisée.</footnote>
## II - DEFINITION DENOTATIONNELLE DE L'INTERPRETATION STANDARD

### II.1 Domaines

Z désigne le domaine des valeurs numériques

$Z = \mathbb{Z}_U\Omega$ Ω désigne l'élément erreur.

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

Par abus tout élément de Z est identifié au nombre syntaxique correspondant. Par exemple, le signe 1 désigne la valeur 1 (élément de Z) où le nombre 1 élément du domaine syntaxique "constantes"

B désigne le domaine des valeurs booléennes

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

L désigne le domaine des positions

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

I désigne le domaine des identificateurs

$i \in I$.

Par abus chaque élément de I est identifié à un élément du domaine syntaxique "variables".

I est un domaine plat

<figure><img src="image_4.png" /></figure>
$R^*$ désigne le domaine des structures

$r^* \in R^* \quad R^* = (Z \times L)^*$

Un élément de $R^*$ est une suite de couples $\langle z, \ell \rangle$ :

la 1<sup>er</sup> composante est une valeur numérique (valeur du selecteur)

la 2<sup>eme</sup> composante est la position de l'élément de la structure désignée par n.

$\perp_S^* = \Lambda$ : suite vide.

D désigne le domaine des valeurs représentables associées à des identificateurs.

$d \in D \quad D = Z+L+B+R^*$

U est le domaine des environnements.

$u \in U \quad U = I \to D \quad \perp_U = \lambda_I \perp_D$

V désigne le domaine des valeurs mémorisables.

$v \in V \quad V = Z+B$

S désigne le domaine des états

$s \in S \quad S = (L \to V) \times \mathbb{Z}^\omega$

Tout élément s de S est un couple $\langle s_1, s_2 \rangle$

ou $s_1$ est la fonction (contenu mémoire) qui associe à chaque position une valeur mémorisable, et $s_2$ est une suite de valeurs (différentes de $\Omega$) qui définit la suite des valeurs qui vont être associées aux paramètres du programme : (fichier d'input)

$\perp_S = \langle \lambda \ell \perp_V, \Lambda \rangle$

E le domaine des expressions est égal à D+V

$e \in E \quad E = D+V$

A désigne le domaine des réponses

$a \in A \quad A = (S \times Z^\omega)$

un élément $a = \langle a_1, a_2 \rangle$ est un couple où

$a_1$ est l'état final

$a_2$ est la suite de valeurs écrites : "output" du programme.

$a_2$ peut contenir le symbole $\Omega$

$\perp_A = (\perp_S, \Lambda)$
C désigne le domaine des continuations d'instructions

$$c \in C \quad C = S \to A \quad \perp_C = \lambda S \perp_A$$

K désigne le domaine des continuations d'expressions

$$k \in K \quad K = E \to C \quad \perp_K = \lambda E \perp_C$$

<table><thead><tr><th>Domaines</th><th>méta variables</th></tr></thead><tbody><tr><td>Z : valeurs arithmétiques</td><td>z</td></tr><tr><td>B : valeurs booléennes</td><td>b</td></tr><tr><td>L : positions</td><td>l</td></tr><tr><td>I : identificateurs</td><td>i*</td></tr><tr><td>R*: structures</td><td>r</td></tr><tr><td>D : valeurs dénotées</td><td>d</td></tr><tr><td>U : environnements</td><td>u</td></tr><tr><td>V : valeurs mémorisables</td><td>v</td></tr><tr><td>S : états</td><td>s</td></tr><tr><td>E : expressions</td><td>e</td></tr><tr><td>A : réponses</td><td>a</td></tr><tr><td>C : continuations d'instruction</td><td>c</td></tr><tr><td>K : continuations d'expression</td><td>k</td></tr></tbody></table>

## II.2 Fonctions auxiliaires

L'écriture des équations sémantiques utilise des fonctions auxiliaires que nous définissons dans ce paragraphe :

* est une fonction de concaténation de type $Z \times Z^* \to Z^*$, par abus de langage. note également la fonction de concaténation de type $R \times R^* \to R^*$

* `hd` de type $(Z^* \to Z_1^*) + (R^* \to R_2^*)$
* `tl` de type $(Z^* \to Z_2^*) + (R^* \to R_1^*)$

### axiomes

$$hd(z \circ z^*) = z$$

$$tl(z \circ z^*) = z^*$$

$$hd(\Lambda) = \perp$$

* `HD` de type $Z^\omega \to Z$
* `TL` de type $Z^\omega \to Z^\omega$

* `cons` est une fonction de concaténation de type $Z^* \times Z^\omega \to Z^\omega$

### axiomes

$$TL(\Lambda) = HD(\Lambda) = \Lambda$$

$$cons(\perp, z^*) = \Lambda$$

$$cons(z, \Lambda) = z$$

$$cons(z \circ z^*, z^*) = cons(z, cons(z^*, z^*))$$
* `hold lS = s↓1(l)` de type `L → S → V`
  Cette fonction donne comme résultat la valeur
  mémorisée à la position `l` dans l'état `s`.

* `content iu = i(u)` de type `I → U → D`
  Fonction analogue à la précédente mais définie
  pour les environnements.

* `update lvs = <s↓1[l\v],s↓2>` de type `L → V → S → S`
  La valeur `v` est associée dans la première composante de `s` à la position `l`: le résultat obtenu est le nouvel état modifié.

* `declare idu : u[i\d]` de type `I → D → U → U`
  La valeur `d` est associée à `i` dans l'environnement `u`.

axiomes

`hold(l update (lvs)) = v`

`l ≠ l' ⇒ hold(l' update (lvs)) = hold l's`

`content (i declare (idu)) = d`

* `give` de type `S → L`
  Chaque appel de cette fonction choisit une position libre `c` est à dire un élément `l` de `L` tel que `hold(l) = l_Y`. Cette fonction est laissée non spécifiée car sa définition implique un choix sur la façon dont les positions sont allouées et ce choix est dépendant d'une implémentation donnée.

* `build z* = z* = Λ → Λ_{R*} <hd(z*), give>build(tl(z*))`
  Cette fonction est de type `Z* → R*`.

* `get s = <HD(s↓2),<s↓1,TL(s↓2)>>` de type `S → V×S`
  Cette fonction donne comme résultat :
  * l'élément le plus à gauche de la suite des valeurs à lire (`HD(s↓2)`)
  * le nouvel état `s` obtenu après amputation de la suite des valeurs à lire de `s`.

* `put z = λcs·<(cs)↓1, cons (z,(cs)↓2)>` de type `Z → C → S → A`.
  La valeur `z` est concatenée à l'élément `(cs)↓2` qui définit la suite des impressions futures.

* `erreur = λs·put(Ω,c, s)` de type `c`
  où `c_0 = λs <s, Λ>`
  lorsque la fonction erreur est activée, la continuation courante est ignorée et l'exécution `s`'arrête avec impression du symbole erreur `Ω`.
$$
\begin{array}{l}
\bullet \quad \text{select } z = \lambda r^* k s \cdot r^* = \Lambda \to \text{erreur}(s), \\
\phantom{\bullet \quad \text{select }} z = hd(r^*) \uparrow 1 \to k(hd(r^*) \uparrow 2)s, \text{select } z tl(r^*)ks \\
\quad \text{de type } Z \to R^* \to K \to A.
\end{array}
$$

Si la valeur z est égale a un selecteur, la
continuation courante est appliquée à l'élé-
ment de L associé à ce selecteur.

II.3 Fonctions sémantiques

Nous associons à chaque domaine syntaxique une fonction qui va
définir la dénotation de chacun des éléments du domaine dans l'interprétation standard.

D : déclarations → U → S → U

EL : 1-expressions → U → K → C

ER : expressions → U → K → C

B : expressions booléennes → U → K → C

C : instructions → U → C → C

P : programmes . → ZZ . → A.

Les domaines syntaxiques "variables" et " constantes" sont identifiés
respectivement aux domaines I et Z.

II.4 Equations

Nous définissons les fonctions énoncées dans le paragraphe précédent
pour chaque construction du langage.

déclarations :

$D[i] = \lambda u \cdot declare(i \ give(s) u)$
L'interprétation de la déclaration d'un identifica-
teur i associe à i dans l'environnement courant u,
la position $\ell$ résultat de la fonction give.

$D[i:n] = \lambda u \cdot declare(izu)$
la valeur z est associée à i dans l'environnement courant.

$D[i[n_1, ..., n_p]] = \lambda u \cdot (\lambda r^* \cdot declare(ir^*u) (build[z_1, ..., z_p]))$
l'élément $r^*$ résultat de la fonction build est associé
à i dans l'environnement courant.

$D[\delta_1; \delta_2] = \lambda u \cdot D[\delta_2] (D[\delta_1] u)$
l-expressions et expressions

Ces deux domaines introduits pour différencier les expressions qui peuvent être affectées (c'est à dire qui ont pour valeur un élément de L) des expressions qui ont pour valeur un élément de V, sont étudiés en parallèle car cette différenciation intervient en cours d'évaluation. La première partie de l'évaluation est commune.

Notons $\mathbb{F}$ la fonction qui a tout élément des domaines expressions et l-expressions associe une fonction de type $U \to K \to \mathbb{C}$

$$ \mathbb{F}[i] = \lambda u k \cdot c(\mathit{ontent} \ i \ u) $$

$$ \mathbb{F}[n] = \lambda u k \cdot kz $$

$$ \mathbb{F}[i[\varepsilon]] = \lambda u k \cdot \mathbb{F}[\varepsilon][u] (\lambda z \cdot \mathit{select} \ z(\mathit{content} \ u \ i)ks)s $$
la valeur de l'index (élément de V) est passée comme argument à la fonction select qui accède dans la structure (résultat de la fonction content) à l'élément désigné.

$$ \mathbb{F}[\varepsilon_1 \rho \varepsilon_2] = \lambda u k \cdot \mathbb{F}[\varepsilon_1][u] (\lambda z_1 \cdot \mathbb{F}[\varepsilon_2][u] (\lambda z_2 \cdot k(z_1 \rho z_2))) $$
l'opérateur sémantique $\rho$ est identifié à l'opérateur $\rho$ syntaxique.

Nous définissons maintenant $\mathbb{EL}$ et $\mathbb{EP}$ en fonction de $\mathbb{F}$.

$$ \mathbb{EL}[\lambda] = \lambda u k \cdot \mathbb{F}[\lambda][u] (\lambda e \cdot e|_L \to k, \mathit{erreur}) $$
Si la valeur résultat de $\mathbb{EL}[\lambda][u]$ est un élément de $L$, l'exécution se poursuit sinon la fonction $\mathit{erreur}$ est exécutée.

$$ \mathbb{EP}[\varepsilon] = \lambda u k \cdot \mathbb{F}[\varepsilon][u] (\lambda e \cdot e|_L \to k(\mathit{hold} \ ls), e|_V \to kes, \mathit{erreur}(s))s $$

Cette fonction force l'évaluation de l'expression jusqu'à ce qu'un élément de V est obtenu : si cet élément ne peut être obtenu, la fonction $\mathit{erreur}$ est exécutée.

Expressions bocléennes

$$ \mathbb{B}[\mathit{true}] = \lambda u k \cdot \mathit{ct} $$

$$ \mathbb{B}[\mathit{false}] = \lambda u k \cdot \mathit{ff} $$

$$ \mathbb{B}[\varepsilon_1 \tau \varepsilon_2] = \lambda u k \cdot \mathbb{B}[\varepsilon_1][u] (\lambda z_1 \cdot \mathbb{B}[\varepsilon_2][u] (\lambda z_2 \cdot k(z_1 \tau z_2))) $$

$$ \mathbb{B}[\beta_1 u \beta_2] = \lambda u k \cdot \mathbb{B}[\beta_1][u] (\lambda b_1 \cdot \mathbb{B}[\beta_2][u] (\lambda b_2 \cdot k(b_1 u b_2))) $$

Remarque :

Un ordre a été imposé pour l'évaluation des opérandes des expressions structurées.
Instructions :

C[null] = λuc·c

C[λ·ε] = λuc·EL[λ]u (λℓ·EP[ε]u (λzs·c.update lns)))

C[if β then γ₁ else γ₂] = λuc·B[β]u (λb·b→C[γ₁]uc, C[γ₂]uc)

C[while β do γ] = λuc·Yg (λg·F[β]u (λb·b → C[γ]ug,c))

ou Yg est l'opérateur plus petit point fixe défini sur C

C input (λ)] = λucs·EL[λ]u (λℓ(λns·c.update lns')) (get s))

la fonction get selecte le premier élément de la suite des valeurs à lire et cet élément est associé dans le nouvel état (résultat de get ) à la position calculée.

C output (ε)] = λucs·EP[ε]u (λz·put(zcs))s

Programme

P[ψ] = λz<sup>ω</sup>·C[γ] (D[δ]⊥s<sub>o</sub>)c<sub>o</sub>s<sub>o</sub>

où s<sub>o</sub> = <⊥, z<sup>ω</sup>> et c<sub>o</sub> = λs·<s, Λ>

le résultat d'un programme ψ interprété avec une suite de valeurs à lire z<sup>ω</sup> est obtenu en interprétant ses instruction dans l'environnement créé par l'interprétation de ses déclarations avec une continuation et un état initiaux.

### III - INTERPRETATION SYMBOLIQUE

L'interprétation symbolique est une extension naturelle de l'interprétation habituelle et consiste à exécuter le programme en donnant aux paramètres des valeurs symboliques. Par analogie avec une interprétation de Herbrand : à chaque constante a est associée la valeur symbolique 'a'

à chaque variable lue est associée une valeur symbolique 'x' (différente pour chaque lecture)

à chaque opérateur f d'arité n on associe l'opérateur 'f' qui définit à partir des termes symboliques 't<sub>1</sub>!', 't<sub>2</sub>', ..., 't<sub>n</sub>' le terme 'ft<sub>1</sub>t<sub>2</sub>...t<sub>n</sub>'.

Une affectation va associer à la variable qui se trouve en partie gauche, le terme résultat de l'interprétation de l'expression qui se trouve en partie droite.

La valeur d'une expression booléenne, dans l'interprétation symbolique ne résulte plus en une constante vrai ou faux ; et donc, lors de l'interprétation symbolique d'une instruction conditionnelle, les deux alternatives sont interprétées en parallèle.
Le résultat peut être vu comme un arbre binaire qui peut être infini si une boucle a été interprétée.

A un noeud non terminal de cet arbre (qui correspond donc à l'interprétation d'une instruction conditionnelle), on associe :

- les termes associés à chacun des identificateurs en ce point de l'interprétation (état de la mémoire).

- la suite, éventuellement vide, des termes qui représentent les résultats partiels produits depuis la construction du noeud précédent c'est à dire depuis l'interprétation de l'instruction conditionnelle précédente.

- le terme résultat de l'interprétation symbolique de l'expression conditionnelle.

**Exemple :**

1. input(X);

2. Y ← 1;

3. while X≠0 do

4. Y ← Y+X;

5. output(Y);

6. X ← X-1;

Notons 'x₁''x₂''x₃''... la suite des valeurs symboliques lues.

- après exécution des instructions 1,2,3,4,5,6 le résultat obtenu est de la forme :

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

$$ \text{où } n_1 = \begin{cases} <X = 'x_1'; Y = '1'> \\ < \Lambda > \\ <'x_1 \neq 0'> \end{cases} $$

$$ n_2 = \begin{cases} <X = 'x_1-1'; Y = '1+x_1'> \\ <'1+x_1'> \\ < \perp > \end{cases} $$

$$ n_3 = \begin{cases} <X = 'x_1'; Y = '1'> \\ < \Lambda > \\ < \perp > \end{cases} $$

Λ désigne la liste vide

⊥ désigne l'élément indéfini du domaine des termes.
- après exécution des instructions 1,2,3,4,5,6,3,4,5,6 c'est à dire
après une deuxième exécution du corps de la boucle le résultat obtenu est de
la forme :

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

où $n_1$ est le noeud défini précédemment

$$n_2 = \begin{cases} <X = 'x_1-1' ; Y = '1+x_1'> \\ <'1+x_1'> \\ <'x_1-1 \neq 0'> \end{cases}$$

$n_3$ est le noeud défini précédemment.

$$n_4 = \begin{cases} <X = 'x_1-1-1' ; Y = '1+x_1+x_1-1'> \\ <'1+x_1+x_1-1'> \\ < \perp > \end{cases}$$

$$n_5 = \begin{cases} <X = 'x_1-1' ; Y = '1+x_1'> \\ < \Lambda > \\ < \perp > \end{cases}$$

## Traitement des structures de données

L'accès à une structure de donnée, par exemple à un tableau, se fait par un index : sa valeur numérique désigne l'élément de la structure. Dans le cas de l'interprétation symbolique la valeur de l'index est un terme : toute expression e qui contient un accès à une structure va être transformée en une expression conditionnelle e', les conditions portant sur l'égalité du terme et des valeurs possibles des sélecteurs.

exemple : notons e l'expression $a[i]+p$ et $v_1, \dots, v_n$ les valeurs possibles des sélecteurs.

e est transformée en

$$ 
\begin{align*}
e' &= \begin{cases} 
    \text{if } i=v_1 \text{ then } a[v_1]+p \\
    \text{else if } i=v_2 \text{ then } a[v_2]+p \\
    \text{else} \\
    \text{else if } i=v_n \text{ then } a[v_n]+p.
\end{cases}
\end{align*} 
$$
Ne voulant pas introduire d'expressions conditionnelles dans notre langage, nous faisons "remonter" les conditions au niveau de l'instruction qui contient l'expression e et nous sommes alors ramené à l'interprétation d'une série d'instructions conditionnelles.

exemple : i ← e

est transformée en :

if i=v₁ then i ← a[v₁]+p

else if i=v₂ then i ← a[v₂]+p

else

else if i=v_n then i ← a[v_n]+p.

# DEFINITION DENOTATIONNELLE DE L'INTERPRETATION SYMBOLIQUE

## III.1 domaines

Z domaine des valeurs symboliques.

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

Par abus Z contient les valeurs symboliques identifiées aux éléments du domaine syntaxique des constantes.

Par exemple la valeur symbolique '1' est identifiée au signe 1.

Z contient également un ensemble de symboles z₁, z₂, ...

T désigne le domaine des termes.

t ∈ T, T = M(Oa,Z) + Ω.

où Oa est l'ensemble des opérateurs arithmétiques symboliques qui sont, par abus, identifiés aux éléments du domaine syntaxique des opérateurs arithmétiques. Le symbole Ω (symbole d'erreur) ne peut apparaître comme sous terme d'un terme t.

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

F désigne le domaine des formules atomiques.

f ∈ F, F = M(Or, T)

où Or est l'ensemble des opérateurs relationnels symboliques identifiés, par abus, aux éléments du domaine syntaxique correspondant.

<figure><img src="image_9.png" /></figure>
B désigne le domaine des valeurs booléennes.

$$b \in B \quad B = M(Ol, F, tt, ff)$$

où chaque élément de $O\ell$ est identifié à un élément du domaine des opérateurs logiques.

un élément $b$ est construit à partir d'expressions relationnelles et des constantes booléennes $tt$ et $ff$.

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

L domaine des positions

$$l \in L.$$

I domaine des identificateurs.

tout élément $i \in I$ est identifié à un élément du domaine syntaxique des variables.

$R^*$ domaine des structures.

$$r^* \in R^* \quad R^* = (Z \times L)^* \quad \bot_R^* = \Lambda$$

D domaine des valeurs dénotées.

$$d \in D \quad D = L+T+B+R^*$$

U domaine des environnements

$$u \in U \quad U = I \to D \quad \bot_U = \lambda I \bot_D$$

V domaine des valeurs mémorisables.

$$v \in V \quad V = T+B$$

S domaine des états.

$$s \in S \quad S = (L \to V) \times Z^\omega$$

La deuxième composante d'un élément $S$ est une suite de valeurs symboliques qui sont par hypothèses différentes les unes des autres, et qui définit la liste des valeurs d'entrées (input)

$$\bot_S = \langle \lambda l \ \bot_V, \Lambda \rangle$$

E domaine des expressions

$$e \in E \quad E = D+V$$
A domaine des réponses

$$ \underline{a \in A} \quad A = (S \times T^{\omega}) + (S \times T^{*}) \times B \times A \times A $$

A = (S×T<sup>ω</sup>) si aucune instruction conditionnelle n'a été exécutée, en effet dans ce cas le résultat est réduit à un seul noeud auquel est associé l'état et la suite des écritures qui ont été produites par l'exécution du programme jusqu'en ce point de l'interprétation.

$$ \text{Sinon } \underline{A} = S \times T^{*} \times B \times A \times A. $$

et un élément $\underline{a}$ est un arbre binaire dont la racine est un élément de $S \times T^* \times F$ et dont les deux descendants sont des éléments de A.

$$ \text{Si } \underline{a} = \langle s, t^*, b, a_1, a_2 \rangle $$

- s désigne l'état qui était l'état courant au moment où $\underline{a}$ a été construit.

- $t^*$ désigne l'écriture effectuée par l'exécution des instructions interprétées entre la construction du prédécesseur de $\underline{a}$ et celle de $\underline{a}$ : c'est donc une écriture partielle.

- b désigne la valeur booléenne calculée lors de l'interprétation symbolique de l'instruction conditionnelle au cours de laquelle l'élément $\underline{a}$ a été construit.

$$ \underline{\perp_A} = \langle \underline{\perp_S}, \Lambda \rangle $$

C domaine des continuations d'instructions

$$ \underline{c \in C} \quad C = S \to A \quad \underline{\perp_C} = \lambda_S \cdot \underline{\perp_A} $$

K domaine des continuations d'expressions

$$ \underline{k \in K} \quad K = E \to C \quad \underline{\perp_K} = \lambda_E \cdot \underline{\perp_C} $$
<table><caption>Tableau récapitulatif :</caption><thead><tr><th>Domaines</th><th>méta variables</th></tr></thead><tbody><tr><td>Z : valeurs symboliques</td><td>z</td></tr><tr><td>T : termes arithmétiques</td><td>t</td></tr><tr><td>F : formules atomiques</td><td>f</td></tr><tr><td>B : termes booléens</td><td>b</td></tr><tr><td>L : position</td><td>l</td></tr><tr><td>I : identificateurs</td><td>i</td></tr><tr><td>R*: structures</td><td>r*</td></tr><tr><td>D : valeurs dénotées</td><td>d</td></tr><tr><td>U : environnements</td><td>u</td></tr><tr><td>V : valeurs mémorisables</td><td>v</td></tr><tr><td>S : états</td><td>s</td></tr><tr><td>E : expressions</td><td>e</td></tr><tr><td>A : réponses</td><td>a</td></tr><tr><td>C : continuations d'instruction</td><td>c</td></tr><tr><td>K : continuations d'expression</td><td>R</td></tr></tbody></table>

Note : Nous avons donné à de nombreux domaines utilisés par la dénotation symbolique, le même nom qu'aux domaines correspondants utilisés par la dénotation habituelle. Ceci a été fait volontairement afin de ne pas alourdir les notations. Le contexte spécifie de quel domaine il s'agit ; et de plus, tout élément intervenant dans la dénotation symbolique est souligné.

### III.2 Fonctions auxiliaires

La plupart de ces fonctions sont identiques à celles utilisées dans la définition dénotationnelle de l'interprétation standard, mais sont définies sur les domaines symboliques.

* fonction de concaténation : $T \times T^* \rightarrow T^*$

$$hd : (T^* \rightarrow T) + (R^* \rightarrow R)$$

$$tl : (T^* \rightarrow T) + (R^* \rightarrow R)$$

$$HD : T^\omega \rightarrow T$$

$$TL : T^\omega \rightarrow T$$
cons : T* × T^ → T^

hold : L → S → V

content : I → U → D

update : L → V → S → S

declare : I → D → U → U

give : S → L

build : Z* → R*

get : S → V × S

put t : λcs <(cs)↓1, (t●(cs)↓2) > cette fonction est du type
T → C → S → A

erreur : C

select t = λr*ks· r* = Λ → erreur(s),

<s,Λ,t=(hd(r*))↓1,k(t↓(r*))↓2 s, select(t t↓(r*)k s)

Cette fonction est du type $T \to R^* \to K \to A$.

Chaque appel de cette fonction définit un élément du domaine

A tel que : - l'état est l'état courant s

- la suite des impressions est la suite vide Λ

- l'expression booléenne est la valeur symbolique
de l'élément de F : t = (hd(r*))↓1 ou t est la valeur de l'index
et (hd(r*))↓1 la valeur du sélecteur.

- la quatrième composante définit l'élément de A
obtenu en appliquant la continuation k à la valeur associée au
sélecteur et à l'état s.

- la cinquième composante définit l'élément de A
résultat de l'appel récursif de la fonction select.

### III.3 Fonctions sémantiques

Une fonction est associée à chaque domaine syntaxique.

D : déclarations → U → S → U

EL : 1-expressions → U → K → C

ER : expressions → U → K → C

R : expressions booléennes → U → K → C

C : instructions → U → C → C

P : programme → T^ω → A.

Les domaines syntaxiques "variables" et " constantes" sont identifiés
respectivement aux domaines I et Z.
### III.4 Equations

#### Déclarations

$$ \underline{D[i]} = \lambda \underline{us} \cdot \underline{declare}(i \ \underline{give}(s) \ u) $$

$$ \underline{D[i:n]} = \lambda \underline{u} \cdot \underline{declare}(i \ \underline{z} \ u) $$

$$ \underline{D[i[n}_1, \dots, n_p]]} = \lambda \underline{u} \ (\lambda \underline{r}^* \cdot \underline{declare}(i \ \underline{r}^* \ u) \ (\text{build } <\underline{z}_1, \dots, \underline{z}_p>)) $$

$$ \underline{D[\delta_1; \delta_2]} = \lambda \underline{u} \cdot \underline{D[\delta_2]} \ (\underline{D[\delta_1]} \underline{u}) $$

#### 1-expressions et expressions

De même que pour la définition de l'interprétation standard nous introduisons une interprétation partielle $\underline{E}$ qui est définie sur les domaines syntaxiques "expressions" et "1-expressions".

$$ \underline{E[i]} = \lambda \underline{uk} \cdot \underline{k} \ (\underline{content} \ i \ u) $$

$$ \underline{E[n]} = \lambda \underline{uk} \cdot \underline{kz} $$

$$ \underline{E[i[\epsilon]]} = \lambda \underline{uks} \cdot \underline{ER[\epsilon]} \underline{u} \ (\lambda \underline{t} \cdot \underline{select} \ t(\underline{content} \ u \ i) \underline{k} \ \underline{s}) \ \underline{s} $$

$$ \underline{E[\epsilon_1 \rho \epsilon_2]} = \lambda \underline{uk} \cdot \underline{ER[\epsilon_1]} \underline{u} \ (\lambda \underline{t}_1 \cdot \underline{ER[\epsilon_2]} \underline{u} (\lambda \underline{t}_2 \cdot \underline{k} \ (\underline{t}_1 \rho \underline{t}_2))) $$

Nous définissons $\underline{EL}$ et $\underline{ER}$ en fonction de $\underline{E}$

$$ \underline{EL}[\lambda] = \lambda \underline{uk} \cdot \underline{E[\lambda]} \underline{u} \ (\lambda \underline{e} \cdot \underline{e} | \underline{L} \to \underline{k} \ \underline{e}, \ \underline{erreur}) $$

$$ \underline{ER[\epsilon]} = \lambda \underline{uks} \cdot \underline{E[\epsilon]} \underline{u} \ (\lambda \underline{e} \cdot \underline{e} | \underline{L} \to \underline{k}(\underline{hold} \ \underline{l} \ \underline{s}), \\ \underline{e} | \underline{V} \to \underline{k} \ \underline{e} \ \underline{s}, \ \underline{erreur}(\underline{s})) \ \underline{s} $$

#### Instructions

$$ \underline{C[nu\ddot{l}l]} = \lambda \underline{u} \ \underline{c} \cdot \underline{c} $$

$$ \underline{C[\lambda \leftarrow \epsilon]} = \lambda \underline{uc} \cdot \underline{EL[\lambda]} \underline{u} \ (\lambda \underline{l} \cdot \underline{ER[\epsilon]} \underline{u} \ (\lambda \underline{ts} \cdot \underline{c}(\underline{update} \ \underline{l} \ \underline{t} \ \underline{s}))) $$

$$ \underline{C[\mathit{if} \ \beta \ \mathit{then} \ \gamma_1 \ \mathit{else} \ \gamma_2]} = \lambda \underline{uc} \cdot \underline{B[\beta]} \underline{u} \ (\lambda \underline{abs} \cdot \langle \underline{s}, \underline{\Lambda}, \underline{b}, \underline{C[\gamma_1]} \underline{ucs}, \underline{C[\gamma_2]} \underline{ucs} \rangle) $$

La définition de $\underline{C}$ appliquée à une structure conditionnelle détermine un élément de $\underline{A}$ tel que :

1. la première composante est l'état courant

2. la suite d'écriture est la suite vide

3. le terme booléen est la valeur de $\beta$.

4. la quatrième composante est l'arbre résultat de l'interprétation de $\gamma_1$ et la suite du programme

5. la dernière composante définit l'arbre résultat de l'interprétation de $\gamma_2$ et de la suite du programme.
$C[\underline{while} \ \beta \ do \ \gamma] =$
$$ \lambda \underline{uc} \cdot Y_g (\lambda g \cdot B[\underline{\beta}]u \ (\lambda \underline{bs} \cdot <s, \Lambda, \beta, C[\underline{\gamma}]ugs, cs>)) $$
où $Y_g$ est l'opérateur plus petit point fixe définit sur $C$

$C[\underline{input} (\lambda)] =$
$$ \lambda \underline{ucs} \cdot EL[\underline{\lambda}]u \cdot (\lambda \underline{b} \cdot (\lambda \underline{zs}' \cdot c(\underline{update} \ lzs'))) (\underline{get} \ s)) $$

$C[\underline{output} (\epsilon)] = \lambda \underline{ucs} \cdot ER[\underline{\epsilon}]u \cdot (\lambda \underline{t} \cdot \underline{put} (t, c, s))$

## Programme

$P[\underline{\psi}] = \lambda z^\omega \cdot C[\underline{\gamma}] \ (D[\underline{\delta}] \perp s_0) \ c_0 \ s_0$

où $c_0 = \lambda s <s, \Lambda>$ et $s_0 = <1, z^\omega>$

# IV RELATION ENTRE L'INTERPRETATION STANDARD ET L'INTERPRETATION SYMBOLIQUE

Nous voulons prouver que pour tout programme, tout résultat obtenu par l'interprétation standard de ce programme peut l'être par une simple valuation v appliquée au résultat de son interprétation symbolique.

Schématiquement :

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

## IV.1 Relation entre les domaines utilisés dans la dénotation de l'interprétation standard et les domaines utilisés dans la dénotation de l'interprétation symbolique.

Notons v la fonction dite de valuation définie d'un domaine symbolique dans un domaine standard.
C'est un morphisme strict.

$$v : \underline{Z} \to Z \qquad v(\underline{z}) = z$$

$$v : \underline{T} \to Z \qquad v(\underline{t_1} \rho \underline{t_2}) = v(\underline{t_1}) \rho v(\underline{t_2})$$

$$v : \underline{B} \to B \qquad v(\underline{t}) = tt$$

$$v(\underline{ff}) = ff$$

$$v(\underline{b_1} \mu \underline{b_2}) = v(\underline{b_1}) \mu v(\underline{b_2})$$

$$v : \underline{L} \to L$$

$$v : \underline{I} \to I$$

### domaines sommes

Si $\underline{X}$ et $X$ sont deux domaines sommes quelconques : $\underline{X} = \underline{X_1} + \underline{X_2}$ et $X = X_1 + X_2$, et si $v_1 : \underline{X_1} \to X_1$, $v_2 : \underline{X_2} \to X_2$, alors $\forall \underline{x} \in \underline{X}$, si $\underline{x} \in E \underline{X_1}$, $v(\underline{x}) = v_1(\underline{x})$

On définit ainsi :

$$v : \underline{D} \to D$$

$$v : \underline{V} \to V$$

$$v : \underline{E} \to E$$

### domaines produits

$$v : (\underline{Z} \times \underline{L}) \to (\underline{Z} \times L) \qquad v(\langle \underline{z}, \underline{l} \rangle) = \langle v(\underline{z}), v(\underline{l}) \rangle$$

et par extension :

$$v : (\underline{Z} \times \underline{L})^* \to (\underline{Z} \times L)^* \qquad v(\langle \underline{z}, \underline{l} \rangle^*) = \langle v(\underline{z}), v(\underline{l}) \rangle^*$$

$$v : \underline{T}^\omega \to \underline{Z}^\omega \qquad v(\underline{t}^\omega) = v(\underline{t})^\omega$$

### domaines fonctionnels

$$v : \underline{U} \to \underline{U} \qquad v(\underline{u}) = \lambda i \cdot v(\underline{u}(i))$$

$$v : \underline{S} \to \underline{S} \qquad v(\underline{s}) = \langle \lambda \underline{l} \cdot v(\underline{s}) \downarrow 1(\underline{l}) \rangle, v(\underline{s}) \downarrow 2(\underline{l})$$

$$v : \underline{C} \to \underline{C} \qquad v(\underline{c}) = \lambda s \cdot v(\underline{c}(s))$$

$$v : \underline{K} \to \underline{K} \qquad v(\underline{k}) = \lambda c \cdot v(\underline{k}(c))$$
### domaines des réponses

$v : A \to A \quad \text{si } a \in E(S \times T^*)$ alors

$$v(s,t) = \langle v(s), \text{cons}(v(t^*), \Lambda) \rangle$$

si $a \in E(S \times T^* \times T \times A \times A)$ alors

$$v(s,t,t,a_1,a_2) = \text{if } v(t) \text{ then}$$

$$\text{let } <s_1,z_1^\omega> = v(a_1) \text{ in}$$

$$<s_1, \text{cons}(v(t^*), z_1^\omega)>$$

else

$$\text{let } <s_2,z_2^\omega> = v(a_2) \text{ in}$$

$$<s_2, \text{cons}(v(t^*), z_2^\omega)>$$

## IV.2 Propriété

Plus précisément, si $v$ est une fonction de valuation définie dans le paragraphe précédent, nous allons montrer que la formule :

$$\forall z^\omega \quad \forall z^\omega \quad v(z^\omega) = z^\omega \implies v(P[\psi]z^\omega) = P[\psi]z^\omega$$

La démonstration utilise une **récurrence structurelle** sur les cons- tructions du langage.

### Lemme 0 :

$$\forall_{S \in S} \quad \forall_{S \in S}$$

$$v(s)=s \implies v(\underline{\text{erreur}}(s)) = \underline{\text{erreur}}(s).$$

démonstration :

Par convention $v(\Omega)=\Omega$ ; d'autre part $v(c_0)=c_0$, le résultat est obtenu en appliquant le lemme 12 (prouvé ultérieurement)

### Lemme 1 :

$$a - \forall \underline{r}^* \in R^* \quad \forall r^* \in R \quad \forall r \in R \quad \forall r \in R$$

$$1. v(\underline{r}^*) = r^* \text{ et } v(\underline{r}) = r \implies v(\underline{r} \cdot \underline{r}^*) = r \cdot r^*$$

$$2. v(\underline{r}^*) = r^* \implies v(hd(\underline{r}^*)) = hd(r^*)$$

$$3. v(\underline{r}^*) = r^* \implies v(tl(\underline{r}^*)) = tl(r^*)$$

$$b - \forall \underline{z}^* \in Z^* \quad \forall \underline{z}^* \in Z^*$$

$$1. v(\underline{z}^*) = z^* \implies v(hd(\underline{z}^*)) = hd(z^*)$$

$$2. v(\underline{z}^*) = z^* \implies v(tl(\underline{z}^*)) = tl(z^*)$$

$$c - \forall \underline{z}^\omega \in Z^\omega \quad \forall \underline{z}^\omega \in Z^\omega$$

$$1. v(\underline{z}^\omega) = z^\omega \implies v(HD(\underline{z}^\omega)) = HD(z^\omega)$$

$$2. v(\underline{z}^\omega) = z^\omega \implies v(TL(\underline{z}^\omega)) = TL(z^\omega)$$

La démonstration de chaque cas se déduit trivialement de la définition de $v$ et des définitions des fonctions.
**Lemme 2 :**

$$ \forall \underline{l} \in \underline{L} \quad \forall \underline{l} \in \underline{L} \quad \forall \underline{s} \in \underline{S} \quad \forall \underline{s} \in \underline{S}. \\ (v(\underline{l})=\underline{l} \text{ et } v(\underline{s})=\underline{s}) \Rightarrow v(\underline{hold} \ \underline{l} \ \underline{s}) = \underline{hold} \ \underline{l} \ \underline{s} $$

$$ \text{démonstration : } v(\underline{s})=\underline{s} \Rightarrow (v(\underline{s}\downarrow 1) = s\downarrow 1 \text{ et } v(\underline{s}\downarrow 2) = s\downarrow 2) \\ \text{et donc } v(\underline{l})=\underline{l} \Rightarrow v(\underline{s}\downarrow 1(\underline{l})) = s\downarrow 1(\underline{l}) $$

**Lemme 3 :**

$$ \forall \underline{i} \in \underline{I} \quad \forall \underline{i} \in \underline{I} \quad \forall \underline{u} \in \underline{U} \quad \forall \underline{u} \in \underline{U} \\ (v(\underline{i})=\underline{i} \text{ et } v(\underline{u})=\underline{u}) \Rightarrow v(\underline{content} \ \underline{i} \ \underline{u}) = \underline{content} \ \underline{i} \ \underline{u} $$

$$ \text{démonstration : } v(\underline{u})=\underline{u} \text{ et } v(\underline{i})=\underline{i} \Rightarrow v(\underline{u}(\underline{i}))=\underline{u}(\underline{i}) $$

**Lemme 4 :**

$$ \forall \underline{l} \in \underline{L} \quad \forall \underline{l} \in \underline{L} \quad \forall \underline{v} \in \underline{V} \quad \forall \underline{v} \in \underline{V} \quad \forall \underline{s} \in \underline{S} \quad \forall \underline{s} \in \underline{S} \\ (v(\underline{l})=\underline{l} \text{ et } v(\underline{v})=\underline{v} \text{ et } v(\underline{s})=\underline{s}) \Rightarrow v(\underline{update} \ \underline{l} \ \underline{v} \ \underline{s}) = \underline{update} \ \underline{l} \ \underline{v} \ \underline{s} $$

$$ \text{démonstration : } v(\underline{s})=\underline{s} \Rightarrow (v(\underline{s}\downarrow 1)=s\downarrow 1 \text{ et } v(\underline{s}\downarrow 2)=s\downarrow 2) \\ \text{comme } v(\underline{l})=\underline{l} \text{ il suffit de proûver que} $$

$v(\underline{s}\downarrow 1(\underline{l}))=s\downarrow 1(\underline{l}) \text{ où } \underline{s}' \text{ est le résultat de } \underline{update} \ \underline{l} \ \underline{v} \ \underline{s}$

$\underline{s}' \text{ est le résultat de } \underline{update} \ \underline{l} \ \underline{v} \ \underline{s}$

ce qui est immédiat d'après la définition des fonctions et l'égalité de $v(\underline{v})$ et $\underline{v}$.

**Lemme 5 :**

$$ \forall \underline{i} \in \underline{I} \quad \forall \underline{i} \in \underline{I} \quad \forall \underline{d} \in \underline{D} \quad \forall \underline{d} \in \underline{D} \quad \forall \underline{u} \in \underline{U} \quad \forall \underline{u} \in \underline{U} \\ (v(\underline{i})=\underline{i} \text{ et } v(\underline{d})=\underline{d} \text{ et } v(\underline{u})=\underline{u}) \Rightarrow v(\underline{declare} \ \underline{i} \ \underline{d} \ \underline{u}) = \underline{declare} \ \underline{i} \ \underline{d} \ \underline{u} $$

la démonstration est immédiate

**Lemme 6 :**

$$ \forall \underline{z}^* \in \underline{Z}^* \quad \forall \underline{z} \in \underline{Z}^* \\ v(\underline{z}^*)=\underline{z}^* \Rightarrow v(\underline{build} \ \underline{z}^*) = \underline{build} \ \underline{z}^* $$

démonstration

1. $\underline{z}^* = \underline{\Lambda}$ alors $v(\underline{z}^*) = \underline{\Lambda}$ et donc d'après l'hypothèse $\underline{z}^* = \underline{\Lambda}$

$\underline{build}(\underline{\Lambda}) = \underline{\Lambda}_R \text{ par définition}$

$\underline{build}(\underline{\Lambda}) = \underline{\Lambda}_R$

$v(\underline{build}(\underline{\Lambda})) = v(\underline{\Lambda}_R) = \underline{\Lambda}_R = \underline{build}(\underline{\Lambda})$
2. $\underline{z}^* = \underline{z} \bullet \underline{z}'^*$ et par hypothèse d'induction

$$ 
\begin{align*}
\nu(\underline{z}^*) &= \underline{z}'^* \implies \nu(\underline{\text{build } \underline{z}'^*}) = \text{build } \underline{z}'^* \\
\nu(\underline{z}^*) &= \underline{z}'^* \implies \nu(\underline{\text{hd}(\underline{z}^*)}) = \text{hd}(\underline{z}^*) \text{ et } \nu(\underline{\text{tl}(\underline{z}^*)}) = \text{tl}(\underline{z}^*) \\
\text{d'après le lemme 1.b}
\end{align*}
$$

$$ \text{et donc } \nu(\underline{hd}(\underline{z}^*), \underline{give}) = \langle hd(z^*), give \rangle $$

En utilisant l'hypothèse d'induction on peut écrire :

$$ \nu(\langle hd(\underline{z}^*), \underline{give} \rangle) \bullet \nu(\text{build}(\underline{z}^*)) = \langle hd(z^*), \underline{give} \rangle \bullet \text{build } \underline{z}'^* $$

ce qui d'après la définition de $\nu$ se réécrit en :

$$ \nu(\text{build } \underline{z}^*) = \text{build } \underline{z}^* $$

**Lemme 7 :**

$$ \forall \underline{u} \in \underline{U} \quad \forall u \in U $$

$$ \nu(\underline{u}) = u \implies \nu(D[[\delta]]) = D[[\delta]] $$

la démonstration se fait par cas sur $\delta$.

a. $\delta::i$

$$ \nu(i) = i \text{ et } \nu(\underline{give}) = \underline{give} \text{ par convention} $$

le résultat est obtenu en appliquant le lemme 4.

b. $\delta::n$

$$ \nu(\underline{z}) = z \text{ par convention} $$

le résultat est obtenu en appliquant le lemme 4.

c. $\delta::i [n_1, \dots, n_p]$

$$ \nu(\underline{z}_1) = z_1 \dots \nu(\underline{z}_p) = z_p \text{ par convention} $$

le résultat s'obtient en appliquant le lemme 6 et le lemme 7.

d. $\delta: \delta_1; \delta_2$.

D'après l'hypothèse d'induction

$$ \forall \underline{u}, u \nu(\underline{u}) = u \implies \nu(D[[\delta_1]]) = D[[\delta_1]] \text{ et } \nu(D[[\delta_2]]) = D[[\delta_2]] $$

$$ \text{et donc } \nu(D[[\delta_1]]\underline{u}) = D[[\delta_1]]u $$

ce qui en appliquant l'hypothèse d'induction implique

$$ \nu(D[[\delta_2]] (D[[\delta_1]]\underline{u})) = D[[\delta_2]] (D[[\delta_1]]u) $$

**Lemme 8 :**

$$ \forall \underline{t} \in \underline{T} \quad \forall \underline{z} \in \underline{Z} \quad \forall \underline{r}^* \in \underline{R}^* \quad \forall \underline{r}^* \in \underline{R}^* \quad \forall \underline{k} \in \underline{K} \quad \forall \underline{k}^* \in \underline{K}^* \quad \forall \underline{s} \in \underline{S} \quad \forall \underline{s}^* \in \underline{S}^* $$

$(\nu(\underline{t})=n \text{ et } \nu(\underline{r}^*)=r^* \text{ et } \nu(\underline{k})=k \text{ et } \nu(\underline{s})=s) \implies \nu(\underline{\text{select }} k \underline{r}^* \underline{r} \underline{s}) = \underline{\text{select }} z \underline{r}^* \underline{r} s$ \\
\text{démonstration}

$$ 
\begin{align*}
\underline{r}^* &= \underline{\Lambda}_R \\
\nu(\underline{\Lambda}_R) &= \underline{\Lambda}_R = z^*
\end{align*}
$$

le résultat est démontré d'après le résultat sur la fonction *erreur*
$$2. \underline{r}^* = \langle \underline{z}_1, \underline{l} \rangle \cdot \underline{r}^{*'} \qquad r^* = \langle \underline{z}_1, \underline{l} \rangle \cdot \underline{r}^{*'}$$

hypothèse d'induction :

($v(\underline{t})=z$ et $v(\underline{r}^*) = \underline{r}^{*'}$ et $v(\underline{k})=k$ et $v(\underline{s})=s \Rightarrow v(\underline{select} \ \underline{t} \ \underline{r}^{*'} \ \underline{k} \ \underline{s}) = \underline{select} \ z \ \underline{r}^{*'}$ ks
$v(\underline{r}^*) = \underline{r}^{*'} \Rightarrow v(\underline{hd}(\underline{r}^*)) = \underline{hd}(\underline{r}^*)$ lemme 1
$\Rightarrow v(\langle \underline{z}_1, \underline{l} \rangle = \langle \underline{z}_1, \underline{l} \rangle$
$\Rightarrow v(\underline{z}_1) = \underline{z}_1$ et $v(\underline{l}) = \underline{l}$ d'après la définition de $v$

$$\text{b-1 Supposons } z=\underline{z}_1=\underline{hd}(\underline{r}^*)\downarrow_2$$

Dans ce cas $v(\underline{t}) = v(\underline{z}_1) - v(\underline{hd}(\underline{r}^*)\underline{z}_1)$

Par définition $\underline{select} \ z \ \underline{r}^* \ k \ s = k \ \underline{hd}(\underline{r}^*)\underline{z}_1 s$

et $v(\underline{select} \ \underline{t} \ \underline{r}^* \ \underline{k} \ \underline{s}) = \underline{let} \ <s_1, z_1^\omega> = v(\underline{k} \ \underline{hd}(\underline{r}^*)\downarrow_2 \ \underline{s}) \ \underline{in}$
$<s_1, \text{cons}(v(\underline{\Lambda}), z_1^\omega)>$
$= <s_1, z_1^\omega>$
$= v(\underline{k} \ \underline{hd}(\underline{r}^*)\downarrow_2 \ \underline{s}) = v(\underline{k} \ \underline{hd}(\underline{r}^*) \ \underline{s})$
$= k \ \underline{hd}(\underline{r}^*) \ \underline{s}$ d'après les hypothèses

$$\text{b-2 Supposons } z \neq \underline{hd}(\underline{r}^*)\underline{z}_1$$

Dans ce cas $v(\underline{t}) \neq v(\underline{hd}(\underline{r}^*)\underline{z}_1)$

Par définition $\underline{select} \ z \ \underline{r}^* \ k \ s = \underline{select} \ z \ \underline{r}^{*'} \ k \ s$.

et $v(\underline{select} \ \underline{t} \ \underline{r} \ \underline{k} \ \underline{s}) = v(\underline{select} \ \underline{t} \ \underline{r}^{*'} \ \underline{k} \ \underline{s})$ avec le même raisonnement que dans le cas précédent, le résultat est prouvé d'après l'hypothèse d'induction.

Lemme 9 :

$$\forall \underline{u} \in \underline{U} \quad \forall \underline{u} \in \underline{U} \quad \forall \underline{k} \in \underline{K} \quad \forall \underline{k} \in \underline{K} \quad \forall \underline{s} \in \underline{S} \quad \forall \underline{s} \in \underline{S}$$

$v(\underline{u})=\underline{u}$ et $v(\underline{k})=\underline{k}$ et $v(\underline{s})=\underline{s} \Rightarrow v(\underline{E}[[\underline{\epsilon}]]) = \underline{E}[[\underline{\epsilon}]]$

La démonstration est faite par cas sur $\underline{\epsilon}$.

a. $\underline{\epsilon}::=i$

Par convention $v(\underline{i})=\underline{i}$. Le résultat est immédiat d'après le lemme 3 et les hypothèses

b. $\underline{\epsilon}::=z$.

Par convention $v(\underline{z})=\underline{z}$ et comme $v(\underline{k})=\underline{k}$, $v(\underline{k} \ \underline{z})=\underline{kz}$.

c. $\underline{\epsilon}::=i[\underline{\epsilon}_1]$

Par hypothèse d'induction on suppose :

$v(\underline{u})=\underline{u}$ et $v(\underline{k})=\underline{k}$ et $v(\underline{s})=\underline{s} \Rightarrow v(\underline{E}[[\underline{\epsilon}_1]]) = \underline{E}[[\underline{\epsilon}_1]]$

On en déduit que $v(\underline{E}[[\underline{\epsilon}_1]]\underline{u}) = \underline{E}[[\underline{\epsilon}_1]]\underline{u}$

Le résultat est obtenu en appliquant les lemmes 3 et 8.
d. $\epsilon ::= \epsilon_1 \rho \epsilon_2$

Par hypothèse d'induction :

$v(u)=u \text{ et } v(k)=k \text{ et } v(s)=s \Rightarrow v(E[[\epsilon_1]]) = E[[\epsilon_1]] \text{ et } v(E[[\epsilon_2]]) = E[[\epsilon_2]]$ et donc

$v(E[[\epsilon_1]]u) = E[[\epsilon_1]]u \text{ et } v(E[[\epsilon_2]]u) = E[[\epsilon_2]]u$

Comme par convention $\rho$ est identifié à $\underline{\rho}$ on peut écrire :

$v(E[[\epsilon_1]]u) \rho v(E[[\epsilon_2]]u) = v(E[[\epsilon_1]]u) \underline{\rho} E[[\epsilon_2]]u$

Le premier membre est égal à

$E[[\epsilon_1]]u \underline{\rho} E[[\epsilon_2]]u.$

Le résultat est obtenu en utilisant $v(k)=k$.

**Lemme 10 :**

$\forall u \in \underline{U}$

$\forall u \in U$

$\forall k \in K$

$\forall k \in K$

$\forall s \in S$

$\forall s \in S,$

$$1. \quad (v(u)=u \text{ et } v(k)=k) \Rightarrow v(E[L[\lambda]]) = E[L[\lambda]]$$

$$2. \quad (v(\underline{u})=u \text{ et } v(k)=k \text{ et } v(s)=s) \Rightarrow v(ER[[\epsilon]]) = ER[[\epsilon]]$$

**Démonstration**

cas 1 - D'après le lemme 9 $v(e)=e$ où $e=\underline{E[[\lambda]]u}$
$e=\underline{E[[\lambda]]u}$

le résultat est obtenu à partir de l'hypothèse $v(k)=k$ et du lemme sur la fonction *erreur*.

cas 2 - D'après le lemme 9 $v(e)=e$.

le résultat est obtenu à partir du lemme 2, des hypothèses et du lemme sur la fonction *erreur*.

**Lemme 11 :**

$\forall u \in U$

$\forall u \in U$

$\forall k \in K$

$\forall k \in K$

$(v(\underline{u})=u \text{ et } v(k)=k) \Rightarrow v(B[[\beta]]) = B[[\beta]]$

**Démonstration**

même raisonnement que pour le lemme 9, mais en faisant une induction sur $\beta$.

**Lemme 12 :**

$\forall t \in T$

$\forall z \in Z$

$\forall a \in A$

$\forall a \in A$

$(v(t)=z \text{ et } v(a)=a) \Rightarrow v(\underline{put}(t,a)) = put(z,a)$
démonstration :

$$1 - \underline{a} \in S \times T^* \times T \times \underline{A} \times \underline{A}$$

$v(\underline{put}(\underline{t}, \underline{a})) = \text{if } v(\underline{t}) \text{ then}$

$$\begin{align*}
\text{let}\langle s_1, z_1^\omega \rangle &= v(\underline{a}_1) \quad \text{in} \\
&<s_1, \text{cons}(v(\underline{t} \cdot \underline{t}^*), z_1^\omega)>
\end{align*}$$

$$\begin{align*}
\text{let}\langle s_2, z_2^\omega \rangle &= v(\underline{a}_2) \quad \text{in} \\
&<s_2, \text{cons}(v(\underline{t} \cdot \underline{t}^*), z_2^\omega)>
\end{align*}$$

$$\text{- si } \underline{t} = \perp$$

$$\begin{align*}
\text{cons}(v(\perp \cdot \underline{t}^*), z_i^\omega) &= \text{cons} \ v(\perp), z_i^\omega \quad \text{pour } i=1,2 \\
&= \text{cons} \ (\perp, z_i^\omega) \\
&= \Lambda
\end{align*}$$

et dans ce cas

$$\begin{align*}
v(\underline{put}(\perp, \underline{a})) &= \langle v(\underline{a}) \downarrow 1, \Lambda \rangle \\
&= \langle a \downarrow 1, \Lambda \rangle \text{ d'après l'hypothèse sur a}
\end{align*}$$

$$\text{Or dans ce cas } \underline{put} (\perp, \underline{a}) = a \downarrow 1, \text{cons}(\perp, a \downarrow 2) = a \downarrow 1, \Lambda$$

$$\text{- si } \underline{t} \neq \perp$$

$$\text{cons}(v(\underline{t} \cdot \underline{t}^*), z_i^\omega) = \text{cons}(v(\underline{t}) \circ v(\underline{t}^*), z_i^\omega)$$

(la distributivité de v et a se déduit des définitions)

$$\begin{align*}
&= \text{cons}(z \circ v(\underline{t}^*), z_i^\omega) \\
&= \text{cons}(z, \text{cons}(v(\underline{t}^*), z_i^\omega))
\end{align*}$$

et dans ce cas

$$\begin{align*}
v(\underline{put}(\underline{t}, \underline{a})) &= \langle v(\underline{a}) \downarrow 1, \text{cons}(z, v(\underline{a}) \downarrow 2) \rangle \\
&= \langle a \downarrow 1, \text{cons}(z, a \downarrow 2) \rangle \text{ d'après l'hypothèse sur a} \\
&= \underline{put}(z, a)
\end{align*}$$

2. $\underline{a} \in S \times T^*$ : c'est un cas particulier du cas précédent.

**Lemme 13 :**

$$\forall s \in S \Rightarrow \forall s \in S$$

$v(s)=s \quad \Rightarrow \quad v(\underline{get} \ s) = \underline{get} \ s.$

preuve triviale d'après le définition des fonctions et le lemme 1-c.

**Lemme 14 :**

$$\forall u \in U \quad \forall u \in U \quad \forall c \in C \quad \forall c \in C \quad \forall s \in S \quad \forall s \in S$$

$$v(u) = u \text{ et } v(c) = c \text{ et } v(s) = s \quad \Rightarrow \quad v(C[\gamma]) = C[\gamma]$$

démonstration :

Elle est faite par cas sur $\gamma$.
f-1 montrons que

$$v(\chi^0(g_o)) = \tau^0(g_o) \text{ où } \chi^0 : \lambda g \otimes \mathbb{1}_c \to \chi^1(g_o)$$

$v(\mathbb{1}_c) = \mathbb{1}_c$ puisque $v$ est une fonction stricte.

f-2 montrons que

$$v(\chi^n(g_o)) = \tau^n(g_o)$$

par hypothèse d'induction :

$$v(\underline{u}) = u \text{ et } v(\underline{c}) = c \text{ et } v(\underline{s}) = s \Rightarrow v(\chi^{n-1}(g_o)) = \tau^{n-1}(g_o)$$

$$\tau^n(g_o) = \mathfrak{B}[\beta]u \quad (\lambda b \quad b \to C[\gamma]\tau^{n-1}(g_o), c)$$

$$\chi^n(\underline{g_o}) = \underline{\mathfrak{B}}[\beta]u \quad (\lambda \underline{b} < \underline{s}, \Lambda, \underline{b}, \underline{C}[\gamma]\chi^{n-1}(\underline{g_o})\underline{s}, \underline{cs})$$

Le résultat est obtenu par une méthode équivalente à celle utilisée pour le cas e.

f-3 $\chi$ et $\tau$ sont des fonctions continues, qui admettent un plus petit point fixe que nous notons "Y"

$$Y(\chi) = \bigcup_{n \ge 0} \chi^n(g_o)$$

$$Y(\tau) = \bigcup_{n \ge 0} \tau^n(g_o)$$

l'égalité étant un prédicat admissible on obtient :

$$v(Y(\chi)) = Y(\tau)$$

$g-\gamma: \gamma_1; \gamma_2$

Par hypothèse d'induction :

$$v(\underline{u}) = u \text{ et } v(\underline{c}) = c \text{ et } v(\underline{s}) = s \Rightarrow v(\underline{C}[\gamma_1]) = C[\gamma_1] \text{ et} \\ v(\underline{C}[\gamma_2]) = C[\gamma_2]$$

et donc

$$v(\underline{C}[\gamma_1]u) = C[\gamma_1]u \text{ et } v(\underline{C}[\gamma_2]u) = C[\gamma_2]u.$$

En utilisant l'hypothèse d'induction :

$$v(\underline{C}[\gamma_2]u, \underline{C}[\gamma_1]u) = C[\gamma_2]u, \underline{C}[\gamma_1]u)$$

Propriété 1 :

$$\forall z \in \mathbb{Z}^\omega \quad \forall \underline{z} \in \underline{\mathbb{Z}}^\omega$$

$$v(\underline{z}^\omega) = \underline{z}^\omega \Rightarrow v(P[\psi]\underline{z}^\omega) = P[\psi]\underline{z}^\omega$$

démonstration :

$v(\underline{\tau}) = \underline{\tau}$ puisque $v$ est une fonction stricte.

Par induction sur la suite des déclarations interprétées et en appliquant le lemme 7 on obtient :

$$v(D[\delta]\underline{\tau}) = D[\delta]\underline{\tau}.$$
D'après l'hypothèse et le fait que $v$ est une fonction stricte
on sait que $v(\underline{s}) = s$

Notons $c_o = \lambda \underline{s} <\underline{s}, \Lambda>$, $c_o = \lambda \underline{s} <\underline{s}, \Lambda>$

si $v(\underline{s})=s$ alors $v(\underline{c_o s})=c_o s$ et donc d'après la définition $v(\underline{c_o})=c_o$

On montre par induction sur la séquence d'instructions interprétée
et en utilisant le lemme 14, que

$v(C[I] (D[I]_1) c_o \underline{s}) = C[I] (D[I]_1) c_o s_o$

ce qui d'après la définition se réécrit en :

$v(P[I]_2 z^\omega) = P[I]_2 z^\omega$

V - INTERPRETATION DE VALIDATION

Cette interprétation est basée sur l'approche utilisée par Wadge
et Shamir pour étudier des propriétés associées aux éléments du domaine des
valeurs (ici Z) de l'interprétation standard. Un ensemble de propriétés
défini à priori est incorporé comme élément du domaine Z. Chaque élément de
ce domaine étendu à deux significations [6] :

1. C'est une donnée sur laquelle des opérateurs sont définis

2. C'est une propriété vérifiée par tous ses approximants :
"x[y" est équivalent à "x à la propriété y" et à "tout objet
qui à la propriété x à la propriété y".

Plus formellement une propriété définie sur Z est un idéal non vide
défini sur Z c'est à dire :

a - J est fermé par le bas : $\forall j \in J \quad \forall z \in Z \quad z[j] \Rightarrow z \in J$

b - J est clos pour les bornes supérieures.

$\forall x y \in J$ si x et y sont compatibles alors
$x \lor y \in J$

On distinguera les idéaux principaux : $\bar{z} = \{z'|z' \underline{[}z\underline{]}\}$.

La structure $T$ des propriétés définies sur Z satisfait

a - $\bar{z} \in T$ ssi $z \in Z$.

b - $z \in T$

c - $T$ est clos pour l'intersection.
Le domaine des valeurs $\hat{z}$ pour cette interprétation est définit par $(T, \Sigma)$ tel que :

a - $\tilde{1}$ est le plus petit élément de $\hat{z}$

b - $\forall z_0 z_1 \in z \quad z_0 \lceil z_1 \rceil \Leftrightarrow \bar{z}_0 \lceil \bar{z}_1 \rceil$

c - si $s$ est un sous ensemble dirigé de $Z$ et $e = \bigcup s$, alors $\{\bar{z} | z \in s\}$ est un sous ensemble dirigé de $\hat{z}$ et $\bar{e}$ est sa borne supérieure.

**Exemple 1 :**

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

si $T$: $\bar{0} \bar{1} \bar{2} \bar{3} \cdots \bar{1-2-3} \cdots \Omega$ positif négatif entier

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

## Extension des opérateurs

Chaque opérateur du langage est étendu sur $\hat{z}$ en fonction de sa
définition sur $Z$.

Si $\rho$ est un opérateur binaire définit sur $Z \times Z \to Z$ et identifié
au signe $\rho$, son extension $\bar{\rho}$ est définie sur $\hat{Z} \times \hat{Z} \to \hat{Z}$ par :

$$ \bar{x} \bar{p} \bar{y} = \bigcup_{n \in \bar{x}} \overline{n \rho m} = \bigcup_{m \in \bar{y}} \overline{n \rho m} \\ \bar{n} \subset \bar{x} \\ \bar{m} \supset \bar{y} $$

**Exemple 2 :**

L'extension de l'opérateur $+$ sur le domaine $\hat{Z}$ décrit dans
l'exemple 1 peut être représentée par :
<table><tr><td>+</td><td>positif</td><td>négatif</td><td>entier positif</td><td>entier négatif</td><td>entier</td><td>1</td></tr><tr><td>positif</td><td>positif</td><td>entier</td><td>positif</td><td>entier</td><td>entier</td><td>1</td></tr><tr><td>négatif</td><td>entier</td><td>négatif</td><td>entier</td><td>négatif</td><td>entier</td><td>1</td></tr><tr><td>entier positif</td><td>positif</td><td>entier</td><td>entier positif</td><td>entier positif entier neg</td><td>entier</td><td>1</td></tr><tr><td>entier négatif</td><td>entier</td><td>négatif</td><td>entier positif entier neg</td><td>entier négatif</td><td>entier</td><td>1</td></tr><tr><td>entier</td><td>entier</td><td>entier</td><td>entier</td><td>entier</td><td>entier</td><td>1</td></tr><tr><td>1</td><td>1</td><td>1</td><td>1</td><td>1</td><td>1</td><td></td></tr></table>

entier positif/entier négatif : c'est un idéal principal qui contient suivant la valeur des opérandes un élément positif ou négatif de Z.

De même les opérateurs relationnels sont étendus sur $\hat{B}$ ou

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

Exemple 3 :

L'extension de l'égalité est définie par :

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

DEFINITION DENOTATIONNELLE DE L'INTERPRETATION DE VALIDATION

V.1 Domaines

$\hat{Z}$ désigne le domaine des propriétés.

$\hat{Z}$ est construit à partir de Z comme il est indiqué dans
le paragraphe précédent.

$\hat{z} \in \hat{Z}$

On notera $\bar{z}$ l'idéal principal associé à l'élément z de Z.
R̂ désigne le domaine des valeurs booléennes.

$$ \hat{\mathbb{B}} \in \hat{\mathbb{B}} $$

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

Ī désigne le domaine des positions

$$ \hat{\ell} \in \hat{\mathbb{L}} $$

Ī est un domaine plat

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

Ī désigne le domaine des identificateurs.

Ī ∈ Ī chaque élément ī est identifié à un élément du domaine syntaxique "variable".

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

R\* désigne le domaine des structures.

$$ \hat{\mathbb{R}} \in \hat{\mathbb{R}}^* \qquad \hat{\mathbb{R}}^* = (\hat{\mathbb{N}} \times \hat{\mathbb{L}})^* = \{\Lambda\} + (\hat{\mathbb{N}} \times \hat{\mathbb{L}}) + (\hat{\mathbb{N}} \times \hat{\mathbb{L}})^2 + \dots $$

Un élément de $\hat{\mathbb{R}}^*$ est une suite de couples $\langle \hat{n}, \ell \rangle$

- la 1ère composante est un élément de $\hat{\mathbb{Z}}$ qui définit la valeur du selecteur.

- la 2ème composante est une position

D̄ est le domaine des valeurs dénotables.

$$ \hat{\mathbb{D}} \in \hat{\mathbb{D}} \qquad \hat{\mathbb{D}} = \hat{\mathbb{Z}} + \hat{\mathbb{L}} + \hat{\mathbb{B}} + \hat{\mathbb{R}} $$

Ū est le domaine des environnements

$$ \hat{\mathbb{U}} \in \hat{\mathbb{U}} \qquad \hat{\mathbb{U}} = \hat{\mathbb{I}} \rightarrow \hat{\mathbb{D}} $$

V̄ est le domaine des valeurs mémorisables.

$$ \hat{\mathbb{V}} \in \hat{\mathbb{V}} \qquad \hat{\mathbb{V}} = \hat{\mathbb{Z}} + \hat{\mathbb{B}} $$

S̄ est le domaine des états

$$ \hat{\mathbb{S}} \in \hat{\mathbb{S}} \qquad \hat{\mathbb{S}} = (\hat{\mathbb{L}} \rightarrow \hat{\mathbb{V}}) \times \hat{\mathbb{Z}}^\omega $$

la 2ème composante de S̄ est la suite des valeurs lues.

$$ \hat{\mathbb{I}} \in \hat{\mathbb{I}} \qquad \hat{\mathbb{V}} = \langle \lambda \hat{\ell} \mid \hat{\mathbb{I}}, \Lambda \rangle $$
Ê est le domaine des expressions

$$ \hat{e} \in \hat{E} \qquad \hat{E} = \hat{D} + \hat{V} $$

Ĉ est le domaine des continuations d'instructions

$$ \hat{c} \in \hat{C} \qquad \hat{C} = \hat{S} \rightarrow \hat{S} $$

K est le domaine des continuations d'expressions

$$ \hat{k} \in \hat{K} \qquad \hat{K} = \hat{E} \rightarrow \hat{C} $$

## V.2 Fonctions auxiliaires

Comme pour les deux interprétations précédentes, nous introduisons des fonctions auxiliaires définies sur les domaines étendus, qui sont utilisées pour l'écriture des équations

* opérateur de concatenation de type $(\hat{Z} \times \hat{Z}^* \rightarrow \hat{Z}^*) + (\hat{R} \times \hat{P}^* \rightarrow \hat{P}^*)$

hd : $(\hat{Z}^* \rightarrow \hat{Z}) + (\hat{R}^* \rightarrow \hat{R})$

tl : $(\hat{Z}^* \rightarrow \hat{Z}^*) + (\hat{R}^* \rightarrow \hat{R}^*)$

HD : $\hat{Z}^\omega \rightarrow \hat{Z}$

CL : $\hat{Z}^\omega \rightarrow \hat{Z}^\omega$

cons : $(\hat{Z} \times \hat{Z}^\omega) \rightarrow \hat{Z}^\omega$

hold : $\hat{L} \rightarrow \hat{S} \rightarrow \hat{V}$

content : $\hat{I} \rightarrow \hat{U} \rightarrow \hat{D}$

update : $\hat{L} \rightarrow \hat{V} \rightarrow \hat{S} \rightarrow \hat{S}$

declare : $\hat{I} \rightarrow \hat{D} \rightarrow \hat{U} \rightarrow \hat{U}$

give : $\hat{S} \rightarrow \hat{L}$

build : $\hat{Z}^* \rightarrow \hat{R}^*$

get : $\hat{S} \rightarrow \hat{V} \times \hat{S}$

erreur : $\hat{S} \rightarrow \hat{A}$

$$ \begin{align*} \text{select } \bar{z} &= \lambda \hat{r} \ \lambda \hat{k} \ \lambda \hat{s} \quad \hat{r} = \Lambda \rightarrow \text{erreur}(\hat{s}), \\ (\bar{z} \hat{=} hd(\hat{r}) \downarrow 1) &= \widehat{tt} \rightarrow \hat{k} \ hd(\hat{r}) \downarrow 2 \ \hat{s}, \\ ((\bar{z} \hat{=} hd(\hat{r}) \downarrow 1) &= \widehat{ff} \rightarrow \text{select } \bar{z} \ tl(\hat{r}) \hat{k} \ \hat{s}, \\ ((\bar{z} \hat{=} hd(\hat{r}) \downarrow 1) &= \widehat{hoo} \rightarrow \hat{k} \ hd(\hat{r}) \downarrow 2 \ \hat{s} \quad \square \\ \text{select } (\bar{z} \ tl(\hat{r}) \hat{k} \ \hat{s}) \end{align*} $$

Cette fonction est du type $\hat{Z} \rightarrow \hat{R}^* \rightarrow \hat{K} \rightarrow \hat{A}$
### V.3 Fonctions

$\hat{D} = \text{déclaration} \rightarrow \hat{U} \rightarrow \hat{U}$

$\hat{EL} = \text{1-expression} \rightarrow \hat{U} \rightarrow \hat{K} \rightarrow \hat{C}$

$\hat{EB} = \text{expression} \rightarrow \hat{U} \rightarrow \hat{K} \rightarrow \hat{C}$

$\hat{B} = \text{expression booléenne} \rightarrow \hat{U} \rightarrow \hat{K} \rightarrow \hat{C}$

$\hat{C} = \text{instructions} \rightarrow \hat{C} \rightarrow \hat{C}$

$\hat{P} = \text{programme} \rightarrow \hat{U} \rightarrow \hat{S} \rightarrow \hat{S}$

Le domaine syntaxique des variables est identifié au domaine I. Chaque constante n est identifiée à l'idéal principal {$z, i$} si dans l'interprétation standard, z est identifié à n.

### V.4 Equations

Les fonctions énoncées précédemment sont définies pour chaque construction du langage.

#### 1 - Déclaration

$\hat{D}[[i]] = \lambda \hat{u}$ déclare $\hat{i}$ give $\hat{u}$

$\hat{D}[[i:n]] = \lambda \hat{u}$ déclare $\hat{i}$ $\hat{z}$ $\hat{u}$.

ou $\hat{z}$ est l'idéal principal définit à partir de n.

$\hat{D}[[i[n_1, \dots, n_p]] = \lambda \hat{u} (\lambda \hat{r}^* \text{ déclare } \hat{i} \hat{r} \hat{u} (\text{build } <\hat{z}_1, \dots, \hat{z}_p>))$

ou $\hat{z}_i$ est l'idéal principal définit à partir de n_i.

$\hat{D}[[\delta_1; \delta_2]] = \lambda \hat{u} \hat{D}[[\delta_2]] (\hat{D}[[\delta_1]] \hat{u})$

Si un identificateur est déclaré plusieurs fois, il n'y a pas génération d'erreur, et la dernière déclaration sera seule utilisée.

#### 2 - 1-expression et expression

De même que pour les dénotations précédentes nous introduisons une première évaluation définie par $\hat{E}$.

$\hat{E}[[i]] = \lambda \hat{u} \lambda \hat{k} \hat{k} (\text{content } \hat{i} \hat{u})$

$\hat{E}[[n]] = \lambda \hat{u} \lambda \hat{k} \hat{k} \hat{z}$

$\hat{E}[[i[\epsilon]] = \lambda \hat{u} \lambda \hat{k} \lambda \hat{s} \hat{E}[[\epsilon]] \hat{u} (\lambda \hat{z} \cdot \text{ select } \hat{z} (\text{content } \hat{u} \hat{i}) \hat{k} \hat{s}) \hat{s}$

$\hat{E}[[\epsilon_1 \rho \epsilon_2]] =$
$\lambda \hat{u} \lambda \hat{k} \hat{E}[[\epsilon_1]] \hat{u} (\lambda \hat{z}_1 \cdot \hat{E}[[\epsilon_2]] \hat{u} (\lambda \hat{z}_2 \cdot \hat{k} (\hat{z}_1 \rho \hat{z}_2)))$
Nous définissons maintenant $\hat{\mathcal{E}}L$ et $\hat{\mathcal{E}}R$ en fonction de $\hat{\mathcal{E}}$.

$$ \hat{\mathcal{E}}L[\lambda] = \lambda\hat{u} \lambda\hat{k} \quad \hat{\mathcal{E}}[\lambda]\hat{u} \quad (\lambda\hat{e} \hat{e} | \hat{\mathcal{L}} \rightarrow \hat{k} \hat{e}, \text{erreur}) $$

$$ \begin{gathered} \hat{\mathcal{E}}R[\varepsilon] = \lambda\hat{u} \lambda\hat{k} \lambda\hat{s} \quad (\lambda\hat{e} \hat{e} | \hat{\mathcal{L}} \rightarrow \hat{k} \quad (\text{hold } \ell \ \hat{s}), \\ \hat{e} | \hat{V} \rightarrow \hat{k} \hat{e}, \\ \text{erreur}) \hat{s} \end{gathered} $$

### 3 - expression booléenne

$\hat{\mathcal{B}}[\text{true}] = \lambda\hat{u} \lambda\hat{k} \quad \hat{k}(\text{tt}) \quad \text{tt est l'idéal principal construit à partir de tt.}$

$\hat{\mathcal{B}}[\text{false}] = \lambda\hat{u} \lambda\hat{k} \quad \hat{k}(\text{ff}) \quad \text{de même ff est construit à partir de ff élément de B)}$

$$ \hat{\mathcal{B}}[\varepsilon_1 \tau \varepsilon_2] = \lambda\hat{u} \lambda\hat{k} \quad \mathcal{E}R[\varepsilon_1]\hat{u} \quad (\lambda\hat{z}_1 \quad \mathcal{E}R[\varepsilon_2]\hat{u} \quad (\lambda\hat{z}_2 \ k(\hat{z}_1 \tau \hat{z}_2))) $$

$$ \hat{\mathcal{B}}[\beta_1 \mu \beta_2] = \lambda\hat{u} \lambda\hat{k} \quad \hat{\mathcal{B}}[\beta_1]\hat{u} \quad (\lambda\hat{b} \cdot \hat{\mathcal{B}}[\beta_2]\hat{u}) \quad (\lambda\hat{b}_2 \quad \hat{k}(\hat{b}_1 \mu \hat{b}_2)) $$

Un ordre arbitraire est imposé pour l'évaluation des opérandes.

### 4 - instruction

$$ \hat{\mathcal{C}}[\text{null}] = \lambda\hat{u} \hat{c} \cdot \hat{c} $$

$$ \hat{\mathcal{C}}[\lambda \leftrightarrow \varepsilon] = \lambda\hat{u} \lambda\hat{c} \quad \mathcal{E}L[\lambda]\hat{u} \quad (\lambda\hat{l} \cdot \hat{\mathcal{E}}R[\varepsilon]\hat{u} \quad (\lambda\hat{z} \quad \hat{c}(\text{update } \hat{l} \hat{z}))) $$

$$ \hat{\mathcal{C}}[\text{output}(\varepsilon)] = \lambda\hat{u} \lambda\hat{c} \cdot \hat{c} $$

$$ \begin{align*} \hat{\mathcal{C}}[\text{if } \beta \text{ then } \gamma_1 \text{ else } \gamma_2] &= \lambda\hat{u} \lambda\hat{c} \quad \hat{\mathcal{B}}[\beta]\hat{u} \quad (\lambda\hat{b} \quad \hat{b} = \text{tt} \rightarrow \hat{\mathcal{C}}[\gamma_1]\hat{u} \quad \hat{c}) \\ & \quad \hat{b} = \text{ff} \rightarrow \hat{\mathcal{C}}[\gamma_2]\hat{u} \quad \hat{c} \\ & \quad \hat{b} = \text{boo} \rightarrow \hat{\mathcal{C}}[\gamma_1]\hat{u} \quad \hat{c} \quad \lor \quad \hat{\mathcal{C}}[\gamma_2]\hat{u} \quad \hat{c} \end{align*} $$

$$ \begin{align*} \mathcal{C}[\text{while } \beta \text{ do } \gamma] &= \lambda\hat{u} \hat{c}(\gamma(\lambda\hat{g} \quad \hat{\mathcal{B}}[\beta]\hat{u} \quad (\lambda\hat{b} \quad \hat{b} = \text{tt} \rightarrow \hat{\mathcal{C}}[\gamma]\hat{u} \quad \hat{g}, \\ & \quad \hat{b} = \text{ff} \rightarrow \hat{c}, \\ & \quad \hat{b} = \text{boo} \rightarrow \hat{\mathcal{C}}[\gamma]\hat{u} \quad \hat{g} \lor \hat{c}))) \end{align*} $$

$$ \mathcal{C}[\gamma_1; \gamma_2] = \lambda\hat{u} \lambda\hat{c} \cdot \hat{\mathcal{C}}[\gamma_1] \quad (\hat{\mathcal{C}}[\gamma_2]\hat{c}) $$

### 5 - programmes

$$ \begin{align*} \hat{\mathcal{P}}[\psi] &= \lambda\hat{z}^\omega \cdot \hat{\mathcal{C}}[\gamma](\hat{\mathcal{D}}[\delta]\perp s_o) \quad \hat{c}_o \\ \text{où } \hat{c}_o &= \lambda\hat{s} \quad \langle\hat{s}, \Lambda\rangle \quad \text{et } \hat{s}_o = \langle\perp, \hat{z}^\omega\rangle \end{align*} $$
# VI. RELATION ENTRE L'INTERPRETATION STANDARD ET L'INTERPRETATION DE VALIDATION

Nous allons prouver que si la propriété $\hat{z}_j$ est associée à l'identificateur $i_j$ dans le résultat de $\hat{P} \llbracket \psi \rrbracket \hat{z}^\omega$, alors pour toute interprétation standard telle que la liste des valeurs lues vérifie $\hat{z}^\omega$, l'état final associe à $i_j$ une valeur qui satisfait la propriété $\hat{z}_j$.

Pour cela nous allons définir une relation entre les domaines utilisés par les deux interprétations.

## VI.1 Relation entre les domaines utilisés dans la dénotation de l'interprétation standard et les domaines utilisés dans la dénotation de l'interprétation de validation

Notons $\Phi$ la fonction qui associe à tout élément $z \in Z$, l'élément $\bar{z}$ de $\hat{Z}$ défini par :

$$ \Phi(z) = \{z' \mid z' \stackrel{\overline{\wedge}}{=} \underline{z}\} $$

$\Phi$ est une fonction stricte.

$$ \Phi : Z \to \hat{Z} \qquad \Phi(z) = \bar{z} $$

$$ \Phi : B \to \hat{B} \qquad \Phi(\overline{tt}) = \overline{\hat{t}} \qquad \Phi(ff) = \overline{\hat{f}} $$

$$ \Phi(b_1 v b_2) = \Phi(b_1) \hat{v} \Phi(b_2) $$

$$ \Phi : L \to \hat{L} $$

$$ \Phi : I \to \hat{I} $$

### domaines sommes

Si $X$ et $\hat{X}$ sont deux domaines quelconques tels que $X : X_1 + X_2$ et $\hat{X} = \hat{X}_1 + \hat{X}_2$, et si $\Phi_1 : X_1 \to \hat{X}_1$

$$ \Phi_2 : X_2 \to \hat{X}_2 $$

$$ \begin{array}{lclcl} \text{alors} & x \in X & \text{si} & x \in X_1 & \Phi(x) = \Phi_1(x) \\ & & \text{si} & x \in X_2 & \Phi(x) = \Phi_2(x) \end{array} $$

On définit ainsi :

$$ \Phi : D \to \hat{D} $$

$$ \Phi : V \to \hat{V} $$

$$ \Phi : E \to \hat{E} $$
### domaines produits

$$ \Phi : (Z \times L) \to \widehat{(Z \times L)} \quad \Phi(<z, \ell>) = \langle \phi(z), \phi(\ell) \rangle $$

et par extension

$$ \Phi : (Z \times L)^* \to \widehat{(Z \times L)}^* \quad \Phi(<z, \ell>^*) = \langle \phi(z), \phi(\ell) \rangle^* $$

$$ \Phi : Z^{\omega} \to \tilde{Z}^{\omega} $$

### domaines fonctionnels

$$ \Phi : U \to \hat{U} \qquad \phi(u) = \lambda i \cdot \Phi(u(i)) $$

$$ \Phi : S \to \hat{S} \qquad \phi(s) = \lambda \ell \cdot \phi(s(\ell)) $$

$$ \Phi : C \to \hat{C} \qquad \Phi(c) = \lambda s \cdot \phi(c(s)) $$

$$ \Phi : K \to \hat{K} \qquad \phi(k) = \lambda \cdot \Phi(k(e)) $$

### domaines des réponses

$$ \Phi : A \to \hat{S} \qquad \phi(a) = \phi(a \downarrow 1) $$

## VI.2 propriété

Nous allons montrer que pour tout programme, le résultat de l'interprétation standard appliquée à une liste de valeurs à lire qui vérifie la propriété $\hat{z}^ω$, vérifie la propriété calculée par l'interprétation de validation de ce programme appliquée à la liste $\hat{z}^ω$.

Plus précisément nous allons montrer que la formule

$$ \forall z^\omega \quad \forall \hat{z}^\omega \quad \Phi(z^\omega)[\hat{z}^\omega] \Rightarrow \Phi(P[\psi]z^\omega)[\hat{P}[\psi]\hat{z}^\omega] $$

est vraie.

La démonstration utilise une récurrence structurelle sur les constructions du langage : la technique est semblable à celle qui est utilisée dans le chapitre IV ; aussi certaines démonstrations ne sont pas réécrites et les lemmes techniques associés aux fonctions auxiliaires ne sont pas énoncés à nouveau.

**Lemme 15 :**

$$ \forall \hat{u} \in \hat{U} \quad \forall u \in U \\ \Phi(u)[\hat{u}] \Rightarrow \Phi(D[\delta])[\hat{D}[\delta]] $$

La démonstration se fait par cas sur $\delta$ en suivant le même raisonnement que dans le paragraphe précédent.
**Lemme 16 :**

$$ 
\begin{array}{l}
\forall z \in Z \quad \forall \hat{z} \in \hat{Z} \quad \forall r^* \in R^* \quad \forall \hat{r}^* \in \hat{R}^* \quad \forall k \in K \quad \forall \hat{k} \in \hat{K} \quad \forall s \in S \quad \forall \hat{s} \in \hat{S} \\
(\phi(z) \underline{[} \hat{z} \text{ et } \phi(r^*) \underline{[} \hat{r} \text{ et } \phi(k) \underline{[} \hat{k} \text{ et } \phi(s) \underline{[} \hat{s} \text{)} \Rightarrow \\
\qquad \qquad \qquad \phi(\text{select } z r^* k s) \underline{[} \text{ select } \hat{z} \hat{r}^* \hat{k} \hat{s}
\end{array}
$$

démonstration

1. $r^* = \Lambda$ alors $\phi(r^*) = \Lambda$
or d'après la structure de $\hat{r}^*$ et l'hypothèse $\phi(r^*) \underline{[} \hat{r}^*$
on en déduit $\hat{r}^* = \Lambda$
Par hypothèse $\phi(s) \underline{[} \hat{s} \text{ donc } \phi(\text{erreur } s) \underline{[} \text{ erreur } \hat{s}.$

2. $r^* = r \cdot r'^*$, $\hat{r}^* = \hat{r} \cdot \hat{r}'^*$
hypothèse d'induction :
$$ (\phi(z) \underline{[} \hat{z} \text{ et } \phi(r') \underline{[} \hat{r}^* \text{ et } \phi(k) \underline{[} \hat{k} \text{ et } \phi(s) \underline{[} \hat{s} \text{)} \Rightarrow \phi(\text{select } z r'^* k s) \underline{[} \text{ select } \hat{z} \hat{r}'^* \hat{k} \hat{s} \\ \phi(r) \underline{[} \hat{r} \text{ donc } \phi(z_1, \ell) \underline{[} (\hat{z}_1, \ell) \text{ ou encore } \phi(z_1) \underline{[} \hat{z}_1 \text{ et } \phi(\ell) = \ell $$

2.1 cas $z = z_1$.
alors soit $(\hat{z} = \hat{z}_1) \hat{=} \overline{tt}$ et dans ce cas le résultat est
obtenu à partir des hypothèses
soit $(\hat{z} = \hat{z}_1) \hat{=} \overline{boo}$ et le résultat est à fortiori vrai.

2.2 cas $z \neq z_1$.
alors soit $(\hat{z} = \hat{z}_1) \hat{=} \overline{ff}$ et dans ce cas le résultat est
obtenu à partir de l'hypothèse de récurrence
soit $(\hat{z} = \hat{z}_1) \hat{=} \overline{boo}$ et le résultat est à fortiori vrai.

**Lemme 17 :**

$$ 
\begin{array}{l}
\forall u \in U \quad \forall \hat{u} \in \hat{U} \quad \forall k \in K \quad \forall \hat{k} \in \hat{K} \quad \forall s \in S \quad \forall \hat{s} \in \hat{S} \\
(\phi(u) \underline{[} \hat{u} \text{ et } \phi(k) \underline{[} \hat{k} \text{ et } \phi(s) \underline{[} \hat{s} \text{)} \Rightarrow \phi(E \underline{[} \hat{\epsilon} \underline{]}) \underline{[} \hat{E} \underline{[} \hat{\epsilon} \underline{]})
\end{array}
$$

La démonstration se fait par cas sur $\epsilon$ et est analogue à celle
du lemme 9.

**Lemme 18 :**

$$ 
\begin{array}{l}
\forall u \in U \quad \forall \hat{u} \in \hat{U} \quad \forall k \in K \quad \forall \hat{k} \in \hat{K} \quad \forall s \in S \quad \forall \hat{s} \in \hat{S} \\
1. \phi(u) \underline{[} \hat{u} \text{ et } \phi(k) \underline{[} \hat{k} \text{)} \quad \Rightarrow \quad \phi(E \underline{[} \hat{\epsilon} \underline{]}) \underline{[} \hat{E} \underline{[} \hat{\epsilon} \underline{]}) \\
2. \phi(u) \underline{[} \hat{u} \text{ et } \phi(k) \underline{[} \hat{k} \text{ et } \phi(s) \underline{[} \hat{s} \text{)} \quad \Rightarrow \quad \phi(E \underline{[} \hat{\epsilon} \underline{]}) \underline{[} \hat{E} \underline{[} \hat{\epsilon} \underline{]})
\end{array}
$$

La démonstration est analogue à celle du lemme 10.
**Lemme 19 :**

$$ \forall u \in U \quad \forall \hat{u} \in \hat{U} \quad \forall k \in K \quad \forall \hat{k} \in \hat{K} \\ (\phi(u)[\hat{u} \text{ et } \phi(k)[\hat{k}]) \Rightarrow \phi(B[[\beta]]) [\hat{B}[[\beta]]] $$

La démonstration est analogue à celle du lemme 11.

**Lemme 20 :**

$$ \forall u \in U \quad \forall \hat{u} \in \hat{U} \quad \forall c \in C \quad \forall \hat{c} \in \hat{C} \quad \forall s \in S \quad \forall \hat{s} \in \hat{S} \\ (\phi(u)[\hat{u} \text{ et } \phi(c)[\hat{c} \text{ et } \phi(s)[\hat{s}]) \Rightarrow \phi(C[[\gamma]]) [\hat{C}[[\gamma]]] $$

La démonstration se fait par cas sur $\gamma$.

a- $\gamma::null$

trivialement vérifié

b- $\gamma:: \lambda \leftrightarrow \epsilon$

c- $\gamma::input(\lambda)$

la démonstration est analogue à celle du lemme 14 cas b et c

d- $\gamma::output(\epsilon)$

il suffit de montrer que

$$ \phi(\text{cs} \downarrow 1) [\hat{c} \hat{s}] $$

ce qui est vérifié d'après les hypothèses et la monotonicité des fonctions.

e- $\gamma:: \text{if } \beta \text{ then } \gamma_1 \text{ else } \gamma_2$

par hypothèse d'induction

$$ (\phi(u)[\hat{u} \text{ et } \phi(c)[\hat{c} \text{ et } \phi(s)[\hat{s}]) \Rightarrow (\phi(C[[\gamma_1]])[\hat{C}[[\gamma_1]]] \text{ et } \\ \phi(C[[\gamma_2]])[\hat{C}[[\gamma_2]]]) ) $$

la démonstration utilise le lemme 17 et est semblable à celle faite pour prouver le lemme 16.

f- $\gamma::while \beta \ do \gamma$

notons $\tau$: la fonctionnelle :

$$ \lambda g. (B[[\beta]]u (\lambda b \cdot b \rightarrow C[[\gamma]]ug, c)) $$

et $\hat{t}$: la fonctionnelle :

$$ \begin{align*} \lambda \hat{g}. (B[[\beta]]\hat{u} (\lambda \hat{b} \hat{b} = \hat{t} \rightarrow \hat{C}[[\gamma]]\hat{u} \hat{g}) \\ \hat{b} = \hat{f} \rightarrow \hat{c}, \\ \hat{b} = \hat{bbo} \rightarrow \hat{C}[[\gamma]]\hat{u} \hat{g} \lor \hat{c}) \end{align*} $$
f-1

$$
\begin{gathered}
\phi(\tau^\circ(g)) = \hat{\tau}^\circ(\hat{g}) \quad \text{avec } \tau_o = \lambda g \perp_c \\
\hat{\tau}_o = \lambda \hat{g} \perp_c
\end{gathered}
$$

f-2

Supposons $\phi(\tau^{n-1}(g_o)) [\hat{\tau}^{n-1}(\hat{g}_o)$

on montre que $\phi(\tau^n(g_o)) [\hat{\tau}^n(\hat{g}_o)$ par une démonstration
analogue à celle du lemme 16.

f-3

$$
\text{notons } Y_g(\tau) = \bigcup_{\tau^n(g_o)} \text{ le plus petit point fixe de } \tau
$$

$$
Y_g(\hat{\tau}) = \bigcup_{\hat{\tau}^n} (\hat{g}_o) \text{ le plus petit point fixe de } \hat{\tau}
$$

$\phi(\tau^n(g_o)) [\hat{\tau}^n(\hat{g}_o)$ est vrai $\forall n$, l'inclusion étant un
prédicat admissible, est vérifié à la limite et donc

$$
\phi(Y_g(\tau)) \subseteq Y_g(\hat{\tau})
$$

g~y:::y1:y2
=========

la démonstration est analogue à celle du lemme 14 cas g.

Propriété 2

$$
\forall z^\omega \quad \forall \hat{z}^\omega
$$

$$
\phi(z^{\omega}) [ \hat{z}^{\omega} \Rightarrow \phi(P[\psi]z^{\omega}) [ \hat{P}[\psi] \hat{z}^{\omega} ]
$$

démonstration :

elle est semblable à celle de la propriété 1, en utilisant les
lemmes 15 et 20.
Conclusion

Nous avons donné pour un langage simple, la définition dénotationnelle
de deux interprétations non-standard et nous avons prouvé les relations qui
existent entre ces deux interprétations et l'interprétation standard.

La sémantique dénotationnelle fournit un outil bien adapté à ce type
de problème : nous poursuivons ce travail par l'étude d'autres types d'interpré-
tation (interprétations statiques...).

Enfin une implémentation de ces interprétations, qui suit fidèlement
leur description dénotationnelle, est en cours de réalisation sur le système
MENTOR [2] construit à l'IRIA.

Remerciements :

Je remercie C.P. Wadsworth et R. Milne pour leurs commentaires et
discussions des premières versions de ce rapport.
Références :

[1] Cousot P. and Cousot R :
"Abstract interpretation : a unified lattice model for static analysis
of programs by construction or approximation of fixpoints".
Proc. ACM Symp. on Principles of Programming Languages
Los Angeles 77 (238-252).

[2] Donzeau-Gouge V., Huet G., Kahn G., Lang B., Lévy J.J., "A structure-oriented program editor : a first step towards computer assisted programming". ICS 75 may 75.

[3] King J.C.
"A new approach to program testing",
Internal conference on reliable software 75

[4] Milne R. and Strachey C.
"A theory of programming language semantics"
Chapman and Hall

[5] Scott D.
"Data types as lattices"
SIAM J. Comput. Vol 5 n°3 Sept. 76 (522-587).

[6] Shamir A. and Wadge W.W.
"Data types as objects"
Tech. report, Computer Science Dept. University of Warwick 77.

[7] Sintzoff M.
"Calculating properties of programs by valuations on specific models"
Proc. ACM Conference on proving assertions about programs.
New Mexico 72, (203-207).

[8] Strachey C. and Wadsworth C.P.
"Continuations- a mathematical semantics for handling full jumps"
Tech. monograph PRG. 11, Programming Research Group,
University of Oxford 74.

[9] Tennent R.D.
"The denotational semantics of programming languages".
Comm. ACM 19, 76 (437-453).

[10] Wechreit B.
"Property extraction in well founded property sets".
IEEE transactions on software engineering
Vol SE-1 n°3 Sept. 75 (270-285).