Previous Up Next

7  Quelle est la sémantique des exceptions?

Donnons d’abord une description intuitive de ce que font les instructions throw et trycatchfinally.

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.

  c::=x=eaffectation simple 
 |x=call  f (x1, …, xn)appel de fonction 
 |c;cséquence 
 |return xretour de fonction 
 |throw Exc (x)lancement d’exception 
 |try c  [catch (Exci xici]1≤ i≤ n finally chandler d’exception

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.

7.1  Sémantique des exceptions en style direct

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  yc 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 xici]1≤ in 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)
Exercice 29   On a dit plus haut que la clause finally serait toujours exécutée. Ce n’est pas le cas si le corps c du try ne termine pas (entre dans un calcul infini), par exemple. Cependant, en ignorant les problèmes de terminaison, montrer qu’il existe quand même des cas où la clause finally ne sera jamais exécutée. Donner des contre-exemples explicites.
Exercice 30   Comment peut-on réparer ceci?

7.2  Sémantique à continuations

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

Exercice 31   Il n’y a pas de règle similaire à (29), laquelle servait à propager les paquets à travers les commandes. Pourquoi, intuitivement?

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.

Exercice 32   Que se passe-t-il si l’exécution de c termine sans passer ni par un return ni par un throw, c’est-à-dire si l’on cherche à appliquer à un environnement? Comparer avec les règles (30) et (31) d’appel de fonction en style direct.

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)
Exercice 33   Démontrer que les deux sémantiques, directe et par continuations, sont équivalents, au sens où: En particulier, si l’on prend comme domaine de réponses l’ensemble des états, et κ la relation identité, en déduire que est dérivable dans la sémantique directe si et seulement si est dérivable dans la sémantique à continuations.

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.

Exercice 34   Démontrer que, si κ est une fonction partielle, alors la relation qui à ρ associe A si et seulement si est déricable dans la sémantique à continuations est elle aussi une fonction partielle.
Exercice 35   Écrire la sémantique des wp de Dijkstra explicitement. Autrement dit, pour chaque forme possible de commande c du langage, donner une définition explicite de wp (c) (κ).
Exercice 36   Démontrer que la sémantique par continuations est monotone en la continuation: si est dérivable, alors pour toute continuation κ+ telle que , alors est aussi dérivable.
Exercice 37   Notre construction de la sémantique par continuations est incomplètement spécifiée. Par exemple, la règle (43) utilise dans sa prémisse une continuation , laquelle n’est définie que lorsque la relation est déjà définie. Or c’est précisément la relation que l’on cherche à définir. Une solution classique dans la littérature est de considérer que de telles règles sont des règles à une infinité de prémisses. Ceci se voit mieux si on réécrit la règle (43) sous la forme:

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.


Previous Up Next