Donnons d’abord une description intuitive de ce que font les
instructions throw
et
try
…catch
…finally
.
D’abord, try
c évalue la commande c, dans
la portée des handlers d’exception décrits par les clauses
catch
et la clause
finally
éventuelle. Si, à l’intérieur de
cette portée, une exception est lancée, par une instruction
throw
exc (val), l’exécution du code se
poursuit dans le handler correspondant: soit le code qui suit une des
clauses catch
(exc x) suivant le bloc c
(avec le même nom d’exception exc; on dit que l’exception est rattrapée par cette clause), en stockant la valeur val de
l’exception dans la variable locale x, soit une des clauses venant
d’un handler d’exception antérieur.
À noter que si C--, comme C, est un langage à liaison
lexicale, c’est-à-dire que la valeur de toute variable est
déterminée par l’endroit, textuel, où on l’utilise, les portées des
handlers d’exception est dynamique. Il est impossible de
savoir vers quel handler d’exception (quelle clause
catch
, quel(s) code(s) de clause
finally
) l’exécution va se brancher lorsqu’une
instruction throw
exc (val) est exécutée.
Ceci est déterminé par la liste active à ce moment-là de l’exécution
du programme. C’est bien entendu voulu.
S’il existe une clause finally
c′, alors le
code c′ sera exécuté chaque fois que l’on sort de la portée du
handler d’exception. C’est le cas lorsque c ne lance aucune
exception (on dit que c termine normalement), lorsque c
lance une exception rattrapée, ou bien lorsque c lance une exception
non rattrapée par le handler courant. Le flot d’exécution du
programme n’est pas modifié (sauf si c′ lance lui-même une
exception!): si l’on passe par le bloc finally
c′ à cause d’une exception non rattrapée, cette exception sera
relancée à la fin de l’exécution de c′; aucune exception n’est
relancée dans les autres cas. Pour mieux comprendre, vous pouvez
exécuter les programmes
exc1,
exc2,
exc3
dans le répertoire d’exemples, avec différents arguments en entrée
(essayez 0, 1, 2, −1 notamment).
Il existe dans la littérature essentiellement deux styles de sémantiques pour décrire l’effet des exceptions.
Le premier consiste à faire comme si une exception lancée était juste une autre forme de résultat. Partant d’un environnement ρ, une commande peut donc s’évaluer soit en un environnement ρ′ après terminaison normale, soit en un paquet d’exception, à savoir un couple formé d’un nom et d’une valeur d’exception, qui a été lancée mais (pas encore) rattrapée. On développe une telle sémantique, dite directe, en section 7.1. Ceci a l’avantage de la simplicité (apparente). C’est le style employé par exemple dans la sémantique de Standard ML, par Harper, Tofte, et Milner.
Le second style consiste à évaluer toute commande c non seulement
relativement à un environnement ρ avant son exécution, mais aussi
relativement au code κ qu’il faudra exécuter une fois l’exécution de
c terminée. Le code κ est la continuation. Un tel style
a été inventée dans les années 1960, précisément pour donner une
sémantique aux exceptions, aux goto
, et autres
joyeusetés du même style, dans le cadre de la sémantique du langage
Algol 60. Cette sémantique, décrite en section 7.2, et
qui part d’une idée a priori plus exotique, a l’avantage d’être plus
souple, au sens où ce style permet de décrire uniformément plusieurs
constructions de flôt de contrôle. De plus, si l’on identifie κ à
l’adresse du code compilé qu’il faudra exécuter une fois c exécuté,
on pourra observer que ce style de sémantique est en fait plus proche
de ce que l’on implémente in fine en assembleur.
Au lieu de traiter de tout le langage C--, par souci de simplicité et de lisibilité, on traitera d’un langage réduit qui ne dispose que des constructions d’exception, de la séquence, et de l’appel de procédure. On laissera en exercice au lecteur le soin d’enrichir la sémantique des autres constructions du langage, en s’inspirant par exemple de la section 6. On ne considérera d’autre part aucun effet de bord, ce qui nous permettra de nous passer de la mémoire, et de revenir à une sémantique à environnement, proche de celle de la section 6.1.
Voici donc la syntaxe des commandes que nous considérons. On suppose donnée une grammaire d’expressions fixée, aucune n’ayant d’effet de bord (x+y OK, x=e non, call f (x) non plus). On peut toujours s’y ramener, par exemple en remplaçant l’expression call f (x) + y par z+y, juste après un appel de fonction z=call f (x), où z est une variable fraîche. Une autre différence est que les retours de fonction return x peuvent être situés au milieu du corps des fonctions. Exc parcourt l’ensemble des noms d’exceptions — en C--, ce sont juste des chaînes de caractères.
|
Ici, un programme π sera une fonction de domaine fini qui à des noms de fonction f associe un couple (l, c), où l est une liste de variables distinctes deux à deux (les paramètres formels de la fonction f), et c est une instruction (le corps de la fonction). On n’aura plus besoin de la troisième composante e, puisque return est maintenant une instruction comme les autres.
Un paquet d’exception est un triplet (ρ, exc, V) formé d’un environnement ρ, d’un nom exc d’exception et d’une valeur V. Un paquet de retour est un triplet (ρ, *, V), où ρ est un environnement, * est un symbole différent de tous les noms d’exception, et V est une valeur. (Ceci sert à représenter l’effet d’une instruction return, qui en un sens est un lancement d’exception.) Un paquet est soit un paquet d’exception soit un paquet de retour. Un état st est soit un environnement ρ, soit un paquet.
L’affectation simple réussit toujours:
où ici comme dans la suite, ρ désigne n’importe quel environnement (mais pas un paquet!). C’est juste la règle (3), inchangée. Contrairement à ce qui se passait en section 6, ce ne sera pas la seule règle qui s’applique sur une affectation (l’autre est (29), plus bas).
Passons directement aux return et aux throw. Ces instructions retournent directement le paquet correspondant.
(26) |
(27) |
Pour la séquence, on aimerait écrire quelque chose de très similaire à (5):
(28) |
La différence est qu’ici, les états intermédiaire st′ et final st″ ne sont pas garantis être des environnements, comme dans (5). Ils pourraient être des paquets, signifiant qu’une exception a été lancée lors de l’exécution de c1 ou de c2. Cependant, la règle ne s’applique que si l’on évalue c1;c2 en partant d’un environnement ρ, pas d’un paquet.
Lorsque l’on cherche à évaluer une commande c en partant d’un paquet, pas d’un environnement, c’est-à-dire que l’on a auparavant lancé une exception, ou déclenché une instruction return, alors c ne sera jamais exécutée. Par exemple, return y; c n’exécutera jamais c. On a besoin pour ceci d’une règle exprimant qu’un paquet passe inchangé à travers toute commande:
(29) |
La notation E ci-dessus dénote soit un nom d’exception Exc, soit *.
On s’attend alors que le corps d’une fonction appelée retourne soit un paquet de retour (ρ, *, V), dénotant un retour normal, soit un paquet d’exception (ρ, Exc, V). Le premier cas est traité par la règle:
(30) |
À noter que l’environnement ρ′ présent dans le paquet de retour (en prémisse) est tout simplement jeté: on n’en voit plus trace dans la conclusion de la règle ci-dessus. C’est parce que ρ′ représente les valeurs des variables locales à la fonction appelée f, qui n’ont plus lieu d’être considérées lors du retour à l’appelant.
Le second cas est traité par la deuxième règle:
(31) |
De même, ici, ρ′ est jeté, et l’on forme un nouveau paquet d’exception avec l’environnement ρ de l’appelant.
Le cœur de la nouvelle sémantique est la définition de throw. On laisse le plaisir au lecteur de comprendre par lui-même ce que signifient ces règles intuitivement.
(32) |
(33) |
(34) |
Ici E′ est soit une exception soit *.
(35) |
On utilise ici un jugement auxiliaire , où [catch (Exci xi) ci]1≤ i≤ n finally c′ n’est, à proprement parler, pas une commande. De plus, on trouve à gauche du symbole un paquet d’exception ρ′, Exc, V et non un environnement.
(36) |
(37) |
(38) |
(39) |
L’idée de la sémantique à continuations est de dériver des jugements de la forme exprimant que c peut s’exécuter de sorte à ce que, lorsque son exécution termine, il ne restera plus qu’à exécuter la suite d’instructions décrites dans la continuation κ, laquelle retourne une réponse A. Cette réponse peut être un environnement final, par exemple. En réalité, une réponse peut être n’importe quel élémént d’un ensemble fixé a priori, qui importe peu.
Formellement, une continuation κ sera juste une fonction qui à chaque état st associe une réponse A: dans le jugement ci-dessus, on trouve la réponse finale A en appliquant κ à l’environnement ρ′ obtenu à la fin de l’exécution de c. (Si c ne lance pas d’exception.) En général, nous ne supposerons pas que la continuation est déterministe, et considérerons κ comme une relation binaire entre états de fin st′ et réponses A. On notera st′ κ A si (st′, A) est dans κ.
L’affectation simple est donc décrite par la règle:
(40) |
Les instructions return et throw ont aussi une description simple:
(41) |
(42) |
Pour la séquence, l’idée est qu’évaluer c1;c2 dans la continuation κ, c’est évaluer juste c1 dans la continuation qui calcule d’abord c2 puis appelle κ. Notons, pour toute commande c, et toute continuation κ, la relation reliant st à A si et seulement si:
On écrit donc:
(43) |
Un petit truc: la prémisse
se lit, intuititivement, “partant de c1, faire c1 puis,
partant de l’environnement ainsi obtenu, faire c2, puis appliquer
κ, obtenant la réponse A”. Une continuation comme
, en pratique, est juste une façon de représenter un saut (jmp
en assembleur) à la fin de l’exécution de c1 vers un morceau de
code qui exécute c2 (puis saute vers le morceau de code dont κ
est une abstraction mathématique).
Là où en section 7.1 nous avions besoin de deux règles pour décrire la sémantique de l’appel de fonctions, nous n’avons plus besoin que d’une règle. On note la relation reliant f (x1, …, xn) à g (x1, …, xn) lorsque x1, …, xn varient dans leur domaine naturel, et P (x1, …, xn) est vrai.
(44) |
L’idée est que, pour exécuter l’appel de fonction, il suffit d’exécuter son corps c. Si l’on finit par exécuter une instruction return, on continuera le calcul en invoquant la continuation κ sur l’environnement ρ [x:=V], poursuivant ainsi le calcul. Si c finit par lancer une exception, c’est κexc qui prendra le relais pour la suite du calcul, laquelle remplace l’environnement ρ′ de la fonction appelée par l’environnement ρ de la fonction appelante.
Les sémantiques à continuations ont été inventées dans les années 1960 pour donner une définition des mécanismes de goto et d’exceptions dans le langage Algol 60. Voyons comment ça se passe. Notons la continuation κ restreinte aux états qui sont des environnements ρ, et κ|Paq la restriction de κ aux paquets, c’est-à-dire la relation reliant tout paquet (E, V) à tout A tel que (E, V) κ A, mais ne reliant aucun environnement ρ à aucune valeur. Finalement, on note la relation κ′ union tous les couples st, A tels que st κ A et st n’est pas dans le domaine de κ′.
(45) |
Si l’on prend comme domaine de réponses l’ensemble des booléens (vrai, faux), et si l’on contraint les continuations κ à être des fonctions partielles (pour tout st, il existe au plus une réponse A telle que st κ A) alors on peut penser aux continuations comme à des tests, ou bien des prédicats. Le jugement se lit “partant de ρ, l’exécution de c peut terminer dans un état vérifiant le prédicat κ”. Les règles de la sémantique à continuations s’interprètent alors comme un calcul connu sous le nom de calcul des “weakest preconditions”, dû à E.W. Dijkstra. Les notations traditionnelles pour ce dernier calcul sont un peu différentes. La “weakest precondition” wp (c) (κ) est par définition le prédicat qui envoie tout état st vers κ (st) si st est un paquet, et si st est un environnement ρ, l’envoie vers vrai si et seulement si est dérivable dans la sémantique à continuations.
Mais ceci n’a aucun sens. En revanche, la règle
(46) |
qui est paramétrée par une continuation κ′, a juste une infinité de prémisses . En utilisant l’exercice 36, justifier pourquoi (46) et (43) sont en fait équivalentes.
En utilisant des règles du style de (46), que vous écrirez, on appellera ensemble des jugements dérivables le plus petit ensemble de jugements stable par les règles de déduction, c’est-à-dire tel que pour toute règle, si toutes ses prémisses sont dans l’ensemble, alors sa conclusion aussi.