II. Sémantique d'un langage de programmation

NB On ne peut donner un sens à un énoncé que s'il est bien typé. Les types sont des éléments essentiels dans la construction des programmes. Ils sont liés à des notions de spécification de de preuve (spécification algébrique de types) que nous développerons dans un chapitre dédié.

La sémantique d'un langage de programmation est ce qui donne la signification aux programmes, les notions permettant de définir formellement les opérations sur les données dans un programme. Dans cd chapitre, on s'intéresse à la sémantique globale d'un programme à partir des composants.

Sémantique dénotationnelle des langages

Définir la sémantique d'un langage est donner la spécification précise de tout énoncé du langage sémantiquement correct. De ce point de vu, la sémantique d'un langage est une fonction de l'ensemble des énoncés sémantiquement corrects vers un autre ensemble supposé connu. Cet autre ensemble est généralement appelé le domaine sémantique du langage considéré.

Dans ce contexte, le domaine sémantique est un domaine mathématique qui permet une description précise et non ambiguë. La sémantique d'un langage est donc une fonction notée :

FIXME : faut trouver les symboles dans LaTeX pour compléter.

On dit que l'énoncé est la notation d'une certaine réalité mathématique et que cette réalité est la dénotation de l'énoncé.

Un aspect important de la sémantique dénotationnelle est la propriété de compositionalité : la dénotation d'un énoncé est obtenu en combinant les dénotations de ses constituants.

Exemple

Considérons le langage des chiffres binaires dont les seuls mots sont “0” et “1”. Posons que nom est “bin” et sa grammaire est :

bin ::  0 | 1

Son domaine sémantique est \left\{0, 1\right\} \in \mathbb{N}

Sa fonction sémantique est définie par (on notera) :

  • \left[\!| 0 |\!\right]_{bin} = 0
  • \left[\!| 1 |\!\right]_{bin} = 1

Considérons le langage des suite binaires maintenant. Appelons “nat” ce langage. Sa grammaire est :

nat ::  bin | nat bin

Son domaine sémantique est \mathbb{N}. Sa fonction sémantique est définie par

  • \left[\!| b |\!\right]_{nat} = \left[\!| b |\!\right]_{bin}
  • \left[\!| n b |\!\right]_{nat} = 2\times \left[\!| n |\!\right]_{nat} + \left[\!| b |\!\right]_{bin}

Exemple

\begin{eqnarray} \left[\!| 1 0 1 |\!\right]_{nat} & = & 2\times \left[\!| 1 0 |\!\right]_{nat} + \left[\!| 1 |\!\right]_{nat} \\ & = & 2\times\left(2\times \left[\!| 1 |\!\right]_{nat} + \left[\!| 0 |\!\right]_{nat}\right) + \left[\!| 1 |\!\right]_{nat} \\ & = & 2\times\left(2\times \left[\!| 1 |\!\right]_{bin} + \left[\!| 0 |\!\right]_{bint}\right) + \left[\!| 1 |\!\right]_{bin} \\ & = & 2\left(2\times 1 + 0 \right) + 1 \\ & = & 5 \end{eqnarray}

fin de l'exemple

L'intérêt de la sémantique dénotationnelle est de faire simplement la preuve des propriétés sur les expressions admises par la syntaxe

  1. les symboles terminaux
  2. les termes construites par les règles de grammaire

Ce type de preuve (démonstration) est appelé démonstration par récurrence ou par induction en mathématiques.

Montrons que pour tout “n” de “nat” la propriété suivante est vraie :
=

On le montre d'abord sur les symboles terminaux (les expressions de “bin”) :

\begin{eqnarray} \left[\!| 0 0 |\!\right]_{nat} & = & 2\times\left[\!| 0 |\!\right]_{nat} + \left[\!|0 |\!\right]_{nat}\\ & = & 2 \times \left[\!| 0 |\!\right]_{bin} +\left[\!| 0 |\!\right]_{nat}\\ & = & 0 +\left[\!| 0 |\!\right]_{nat} \\ & = & \left[\!| 0 |\!\right]_{nat} \end{eqnarray} \qquad \begin{eqnarray} 0 1 _{nat} & = & 2\times 0 _{nat} + 1 _{nat}\\ & = & 2 \times 0 _{bin} + 1 _{nat}\\ & = & 0 + 1 _{nat} \\ & = & 1_{nat} \end{eqnarray}

On le montre ensuite pour les termes construits par les règles de grammaire, ici la règle nat :: nat bin. Supposons que pour un certain n de nat la propriété est vraie. Alors montrons que elle est vraie pour la suite binaire n b.

\left[\!| 0 n b |\!\right]_{nat} = 2\times \left[\!| 0 n |\!\right]_{nat} + \left[\!| b |\!\right]_{nat} par la définition de \left[\!| n |\!\right]_{nat}
= 2 \times \left[\!| n |\!\right]_{nat} + \left[\!| b |\!\right]_{nat} par hypothèse sur n
= \left[\!| n b |\!\right]_{nat} par la définition de \left[\!| \cdot |\!\right]_{nat}

Puisque la propriété est vraie pour les symboles terminaux, elle est ainsi vraie pour tout n de nat.

Autre exemple de preuve par induction

Considérons une fonction définie sur les expression de nat par :

  • succ(0) = 1
  • succ(1) = 1 0
  • succ(n 0 ) = n 1
  • succ( n 1) = succ(n) 0

Essayons de montrer que pour tous n de nat la propriété suivante est vraie : \left[\!| succ( n ) |\!\right]_{nat} = \left[\!| n |\!\right]_{nat} + 1

  • \left[\!| succ(0) |\!\right]_{nat} = \left[\!| 1 |\!\right]_{nat} = \left[\!| 1 |\!\right]_{bin} = 1 = 0 + 1 = \left[\!| 0 |\!\right]_{bin} + 1 = \left[\!| 0 |\!\right]_{nat} + 1
  • \left[\!| succ(1) |\!\right]_{nat} = \left[\!| 1 0 |\!\right]_{nat} = 2\times \left[\!| 1 |\!\right]_{nat} + 0 = 2 = 1 + 1 = \left[\!| 1 |\!\right]_{nat} + 1

Maintenant, supposons la propriété pour un certainn de nat

  • \left[\!| succ(n 0) |\!\right]_{nat} = \left[\!| n 1 |\!\right]_{nat} par définition
    • = 2\times \left[\!| n |\!\right]_{nat} + \left[\!| 1 |\!\right]_{nat}
    • = 2\times \left(\left[\!| n |\!\right]_{nat} + 0 \right) + \left[\!| 1 |\!\right]_{nat}
    • = \left[\!| n 0 |\!\right]_{nat} + 1
  • \left[\!| succ(n 1) |\!\right]_{nat} = \left[\!| succ(n) 0 |\!\right]_{nat}
    par définition de succ( )
    • = 2\times \left[\!| succ(n) |\!\right]_{nat} + \left[\!| 0 |\!\right]_{nat}
      par la règle de grammaire
    • = 2\times \left(\left[\!| n |\!\right]_{nat} + 1 \right) + \left[\!| 0 |\!\right]_{nat}
      par hypothèse de récursion/induction
    • = \left(2\times \left[\!| n |\!\right]_{nat} + 1 \right) + 1 + 0
    • = \left(2\times \left[\!| n |\!\right]_{nat} + \left[\!| 1 |\!\right]_{nat} \right) + 1 = \left[\!| n 1 |\!\right]_{nat} + 1

Constat

Rappel:

  • \left[\!| b |\!\right]_{nat} = \left[\!| b |\!\right]_{bin},
  • \left[\!| n b |\!\right]_{nat} = 2\times \left[\!| n |\!\right]_{nat} + \left[\!| b |\!\right]_{nat}

Cette définition de la sémantique est structurelle et compositionnelle parce qu'elle est fondée sur les règles de grammaire et la sémantique d'une expression ne dépend que de la sémantique des ses sous-expressions. \left[\!| n b |\!\right]_{nat} ne dépend que de \left[\!| n |\!\right]_{nat} et de \left[\!| b |\!\right]_{bin} .

La façon de décrire la syntaxe influe sur la définition de la sémantique. Par exemple, une autre grammaire pour le langage nat est nat :: bin | bin nat mais avec elle la définition de la sémantique aurait été plus compliquée, elle suppose d'exprimer le poids du chiffre binaire b.


Fondements de la programmation « » Sémantique Dénotationnelle d'un langage de programmation

 
m1ilc/semantics_2.txt · Dernière modification: 2010/05/24 08:19 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki