Département d'Informatique
Maîtrise d'Informatique 2001/2002
Spécifications formelles, preuves
& construction de programmes
Travaux dirigés
Mercredi 31 octobre








Sémantique dénotationnelle






Où l'on cherche à définir la sémantique d'un langage dont la syntaxe est donnée par des régles de grammaire. Cette sémantique peut être utilisée pour faire la preuve (éventuellement par induction) de propriétés sur les expressions admises par la syntaxe.

1   Sémantique de petits langages

1.1   Le langage "nat" des suites binaires

La grammaire de ce langage est donnée ci-dessous: 
  bin :: 0 | 1
  nat :: bin | nat bin
  1. Donner la sémantique dénotationnelle de ce langage.
    Vérifier pour exemple que [[110]] = 6.
  2. Montrer que, pour tout "n" de "nat", [[n0]] = 2×[[n]].
  3. En s'inspirant de l'exemple de la fonction "succ" (successeur) dont la définition est rappelée ci-dessous, définir la fonction "add" (addition de 2 suites binaires). 
    succ(0)  = 1
succ(1)  = 10
succ(n0) = n1
succ(n1) = succ(n)0
  4. Montrer que, pour tout "n", "m" de "nat", [[add(n,m)]] = [[n]] + [[m]].

1.2   Les expressions arithmétiques "exp" de LISP

On considère le langage dont la syntaxe est définie par la grammaire suivante: 
  nbr  :: 0 | 3.14 | -7 | ...
  exp  :: nbr | (+ exp exp) | (- exp exp) | (* exp exp) | (/ exp exp)
  1. Déterminer le domaine sémantique de ce langage, puis donner une définition sémantique structurelle (est-elle compositionnelle ?).

  2. Calculer [[(* (+ 2 1) (/ 6 3))]] ? Que diriez-vous à propos de la sémantique de l'expression (* (+ 2 1) (/ 6 0)) ?
  3. Montrer que, quelles que soient les expressions "e1","e2", "e3" de ce langage:
    [[(+ e1 (+ e2 e3))]] = [[(+ (+ e1 e2) e3)]]

2   Sémantique d'un langage impératif

  1. Utiliser les définitions sémantiques du langage "L" (voir le cours), pour:

    1. déterminer la sémantique des programmes suivants:

      1. x:=1;y:=2;z:=x;x:=y;y:=z
      2. if x<y then skip else x:=y
      3. x:=1;n:=3;do n times x:=2*x

    2. démontrer que, dans chacun des cas suivants, les 2 programmes sont équivalents:
      1. x:=1;y:=2;z:=x;x:=y;y:=z et x:=2;y:=1;z:=1
      2. if x<y then skip else x:=y et if x>=y then x:=y
      3. x:=1;n:=3;do n times x:=2*x et
        x:=1;x:=x*2;x:=x*2;x:=x*2;n:=3

  2. Montrer comment étendre le langage "L" avec la structure de contrôle "repeat A until b".

  3. Déterminer la sémantique du programme suivant: 
    i:=0;f:=1;
while i<n do { i:=i+1;f:=f*i }
  4. Même exercice que précédemment, avec le programme suivant : 
    k:=0;x:=0;
while k<n do { k:=k+1;x:=x+2*k-1 }
This document was translated from LATEX by HEVEA.