Examen de Sémantique des langages séquentiels de janvier 2001


Tous documents autorisés. Durée 3h.


Exercice 1

Soit S une signature contenant la constante a et l'opérateur S d'arité 1. L'ensemble E est construit comme la fermeture inductive du singleton {a} par l'opérateur S.
  1. Donner deux manières de définir l'ensemble E. Est-ce que E correspond à un ensemble bien connu ?
  2. On définit sur E deux fonctions f et g comme suit :
    f(a) = a, g(a) = a
    "t Î E Ù t¹a, (f(S(t))=g(t) Ù g(S(t))=f(t))
    Démontrer que ces équations définissent bien f et g. Donner une définition plus simple (non récursive) de f et g.
Exercice 2

Voici le texte d'une fonction en OCaml :
let rec h = function
| (true,n) -> h(false,n+1)
| (false,0) -> 0
| (false,p) -> h(flase,p-1)+1
  1. Faire la preuve que cette fonction est bien définie i.e. que toute application de cette fonction à un argument termine.
  2. Donner ensuite une définition beaucoup plus simple de h et démontrer, par un raisonnement de même nature que celui de la question précédente, que les deux définitions proposées construisent la même fonction (i.e. ne pas chercher à donner une définition sémantique des fonctions).
Exercice 3

Soit V un ensemble d'identificateurs et int le domaine des entiers. Soient v, w des identificateurs et n et p des entiers.
En sémantique opérationnelle, un environnement, noté ici L et appelé env-op, est une liste d'association définie par les règles d'inférence suivantes. L'environnement vide est dénoté par nil.

En sémantique dénotationnelle, un environnement, noté ici s et appelé env-det, est une fonction totale de v dans int^.
La fonction bot est la fonction constante sur V qui retourne ^.
La fonction maj est définir par :
maj(s,v,n)(v)=n
maj(s,v,n)(w)=s(w) si w¹v
On se donne une onction de traduction T sur les env-op à valeurs dans les env-det définie comme suit :
T(nil)=bot, bot:V->^
T(L1)=maj(T(L2),v,n si L1=(v,n).L2
  1. Montrer que, quels que soient L, v, n, (L|-v->n) <=> (T(L)(v)=n)
  2. Soit un langage d'expressions arithmétiques contenant des constantes (n), des identificateurs (v) e un opérateur mult d'arité 2. On ajoute les règles de sémantique opérationnelle suivantes :

    Donner la sémantique dénotationnelle directe, notée S, de ce langage.
    Montrer rigoureusement que si L est un env-op, e une expression du langage et n une valeur entière, alors :
    (L|-e->n) <=> (S[e](T(L))=n)
Exercice 4

Soit X un ensemble d'identificateurs. Soit S la définition en sémantique directe du langage de programmation vu en cours.
Montrer que pour tout identificqteur x, S[while(1<0) do x:= x] = ly.y

Exercice 5

Rappeler informellement la déifnition du passage de paramètres par référence.
Donner ensuite les définitions en sémantique dénotationnelle directe de la déclaration et de l'appel d'une procédure, ayant un seul paramètre, qui est passé par référence.