“doc” (Col. : Science Sup 17x24) — 2007/7/19 — 18:18 — page 35 — #45
i
i
i
i
i
i
i
i
2.1 Définir un langage de programmation pratique
35
espace et en temps de l’implémentation. Le langage noyau et les structures de
données qu’il manipule sont appelés le modèle de calcul noyau.
– Ensuite, définissez un schéma de traduction du langage pratique complet vers le
langage noyau. Chaque construction grammaticale dans le langage complet est
traduite dans le langage noyau. La traduction doit être simple. Il y a deux formes
de traduction, que nous appelons l’abstraction linguistique et le sucre syntaxique.
Nous les expliquons ci-dessous.
Chaque modèle de calcul du livre a son propre langage noyau. On l’obtient simplement
en ajoutant un nouveau concept à un langage noyau qui le précède. Le premier, présenté
dans ce chapitre, s’appelle le langage noyau déclaratif. Nous en présenterons plusieurs
autres plus loin.
La sémantique formelle
Nous avons la liberté de définir la sémantique du langage noyau comme nous le
voulons. Il y a quatre approches largement utilisées pour la sémantique des langages
de programmation :
– Une sémantique opérationnelle montre comment une instruction s’exécute sur
une machine abstraite. Cette approche fonctionne toujours bien, parce que tous
les langages s’exécutent sur un ordinateur.
– Une sémantique axiomatique définit le sens d’une instruction comme une relation entre l’état de l’entrée (avant l’exécution de l’instruction) et l’état de la
sortie (après l’exécution de l’instruction). Cette relation est donnée comme une
assertion logique. C’est une bonne manière de raisonner sur les séquences d’instructions, parce que la sortie de chaque instruction est l’entrée de l’instruction
suivante. Cette sémantique fonctionne bien pour les modèles avec état, parce
qu’un état est une séquence de valeurs.
– Une sémantique dénotationnelle définit une instruction comme une fonction
sur un domaine abstrait. Cette approche fonctionne particulièrement bien pour
les modèles déclaratifs, mais elle peut être adaptée pour les autres modèles aussi.
L’approche devient compliquée pour les langages concurrents.
– Une sémantique logique définit une instruction comme une relation qui est vraie
sur un modèle logique et son exécution comme une théorie de preuve. Cette
approche fonctionne bien pour les modèles déclaratifs et relationnels, mais est
plus difficile à adapter pour les autres.
Une grande partie de la théorie mathématique de ces sémantiques est intéressante
principalement pour les mathématiciens et non pour les programmeurs. La sémantique
formelle que nous donnons est une sémantique opérationnelle. Nous la définissons pour
chaque modèle de calcul. Elle est assez détaillée pour permettre le raisonnement sur
© Dunod – La photocopie non autorisée est un délit
i
i
i
i
i
i
i
i
2.1 Définir un langage de programmation pratique
35
espace et en temps de l’implémentation. Le langage noyau et les structures de
données qu’il manipule sont appelés le modèle de calcul noyau.
– Ensuite, définissez un schéma de traduction du langage pratique complet vers le
langage noyau. Chaque construction grammaticale dans le langage complet est
traduite dans le langage noyau. La traduction doit être simple. Il y a deux formes
de traduction, que nous appelons l’abstraction linguistique et le sucre syntaxique.
Nous les expliquons ci-dessous.
Chaque modèle de calcul du livre a son propre langage noyau. On l’obtient simplement
en ajoutant un nouveau concept à un langage noyau qui le précède. Le premier, présenté
dans ce chapitre, s’appelle le langage noyau déclaratif. Nous en présenterons plusieurs
autres plus loin.
La sémantique formelle
Nous avons la liberté de définir la sémantique du langage noyau comme nous le
voulons. Il y a quatre approches largement utilisées pour la sémantique des langages
de programmation :
– Une sémantique opérationnelle montre comment une instruction s’exécute sur
une machine abstraite. Cette approche fonctionne toujours bien, parce que tous
les langages s’exécutent sur un ordinateur.
– Une sémantique axiomatique définit le sens d’une instruction comme une relation entre l’état de l’entrée (avant l’exécution de l’instruction) et l’état de la
sortie (après l’exécution de l’instruction). Cette relation est donnée comme une
assertion logique. C’est une bonne manière de raisonner sur les séquences d’instructions, parce que la sortie de chaque instruction est l’entrée de l’instruction
suivante. Cette sémantique fonctionne bien pour les modèles avec état, parce
qu’un état est une séquence de valeurs.
– Une sémantique dénotationnelle définit une instruction comme une fonction
sur un domaine abstrait. Cette approche fonctionne particulièrement bien pour
les modèles déclaratifs, mais elle peut être adaptée pour les autres modèles aussi.
L’approche devient compliquée pour les langages concurrents.
– Une sémantique logique définit une instruction comme une relation qui est vraie
sur un modèle logique et son exécution comme une théorie de preuve. Cette
approche fonctionne bien pour les modèles déclaratifs et relationnels, mais est
plus difficile à adapter pour les autres.
Une grande partie de la théorie mathématique de ces sémantiques est intéressante
principalement pour les mathématiciens et non pour les programmeurs. La sémantique
formelle que nous donnons est une sémantique opérationnelle. Nous la définissons pour
chaque modèle de calcul. Elle est assez détaillée pour permettre le raisonnement sur
© Dunod – La photocopie non autorisée est un délit