“doc” (Col. : Science Sup 17x24) — 2007/7/19 — 18:18 — page 111 — #121
i
i
i
i
i
i
i
i
3.1 La déclarativité c’est quoi ?
111
Il est plus difficile de manipuler les programmes fonctionnels ou logiques que les
programmes descriptifs, mais ils respectent toujours des lois algébriques simples.
3
Notre modèle déclaratif couvre les deux styles, fonctionnel et logique.
La vue observationnelle nous permet d’utiliser des composants déclaratifs dans
un programme déclaratif même s’ils sont écrits dans un modèle non déclaratif. Par
exemple, une interface à une base de données peut être une extension valable à un
langage déclaratif. Cependant, l’implémentation de cette interface n’est probablement
pas logique ou fonctionnelle. Là n’est pas la question. Il suffit qu’elle ait pu être définie
déclarativement. Parfois un composant déclaratif sera écrit dans un style fonctionnel
ou logique. Dans les chapitres ultérieurs nous construisons des composants déclaratifs
dans des modèles non déclaratifs. Nous ne serons pas dogmatiques à ce sujet ; nous
considérerons un composant comme déclaratif s’il se comporte de façon déclarative.
3.1.2 Les langages de spécification
Les partisans de la programmation déclarative prétendent parfois qu’elle permet de
se passer de l’implémentation parce qu’il n’y a que la spécification. Il disent que la
spécification est un programme. C’est vrai en théorie, mais pas en pratique. En pratique,
les programmes déclaratifs sont très semblables à d’autres programmes : ils ont besoin
d’algorithmes, des structures de données et d’un raisonnement sur les opérations.
Cette ressemblance existe parce que les langages déclaratifs doivent se restreindre
aux mathématiques avec une implémentation efficace. Il y a un compromis entre
l’expressivité et l’efficacité. Les programmes déclaratifs sont généralement beaucoup
plus longs par rapport à ce que pourrait être une spécification. Nous concluons que la
distinction entre spécification et implémentation a toujours un sens, même pour les
programmes déclaratifs.
Il est possible de définir un langage déclaratif qui soit bien plus expressif que
celui que nous utilisons. Un tel langage s’appelle un langage de spécification. Il
est généralement impossible de faire une implémentation efficace d’un langage de
spécification. Cela ne veut pas dire qu’un tel langage n’est pas pratique. Au contraire,
c’est un outil important pour réfléchir sur les programmes. On peut l’utiliser avec
un prouveur de théorèmes, qui est un programme qui peut faire certaines formes
de raisonnement mathématique. Les prouveurs de théorèmes pratiques ne sont pas
complètement automatiques ; ils ont besoin d’un coup de main humain. Mais ils
peuvent prendre sur eux une grande partie de la corvée du raisonnement sur les
programmes : la manipulation fastidieuse des formules mathématiques. Avec l’aide
d’un prouveur de théorèmes, un développeur peut souvent prouver des propriétés très
fortes de son programme. Une telle utilisation d’un prouveur de théorèmes s’appelle
l’ingénierie des preuves. Pour l’instant, l’ingénierie des preuves n’est pratique que
3. Si on n’utilise pas les possibilités non déclaratives de ces langages !
© Dunod – La photocopie non autorisée est un délit
i
i
i
i
i
i
i
i
3.1 La déclarativité c’est quoi ?
111
Il est plus difficile de manipuler les programmes fonctionnels ou logiques que les
programmes descriptifs, mais ils respectent toujours des lois algébriques simples.
3
Notre modèle déclaratif couvre les deux styles, fonctionnel et logique.
La vue observationnelle nous permet d’utiliser des composants déclaratifs dans
un programme déclaratif même s’ils sont écrits dans un modèle non déclaratif. Par
exemple, une interface à une base de données peut être une extension valable à un
langage déclaratif. Cependant, l’implémentation de cette interface n’est probablement
pas logique ou fonctionnelle. Là n’est pas la question. Il suffit qu’elle ait pu être définie
déclarativement. Parfois un composant déclaratif sera écrit dans un style fonctionnel
ou logique. Dans les chapitres ultérieurs nous construisons des composants déclaratifs
dans des modèles non déclaratifs. Nous ne serons pas dogmatiques à ce sujet ; nous
considérerons un composant comme déclaratif s’il se comporte de façon déclarative.
3.1.2 Les langages de spécification
Les partisans de la programmation déclarative prétendent parfois qu’elle permet de
se passer de l’implémentation parce qu’il n’y a que la spécification. Il disent que la
spécification est un programme. C’est vrai en théorie, mais pas en pratique. En pratique,
les programmes déclaratifs sont très semblables à d’autres programmes : ils ont besoin
d’algorithmes, des structures de données et d’un raisonnement sur les opérations.
Cette ressemblance existe parce que les langages déclaratifs doivent se restreindre
aux mathématiques avec une implémentation efficace. Il y a un compromis entre
l’expressivité et l’efficacité. Les programmes déclaratifs sont généralement beaucoup
plus longs par rapport à ce que pourrait être une spécification. Nous concluons que la
distinction entre spécification et implémentation a toujours un sens, même pour les
programmes déclaratifs.
Il est possible de définir un langage déclaratif qui soit bien plus expressif que
celui que nous utilisons. Un tel langage s’appelle un langage de spécification. Il
est généralement impossible de faire une implémentation efficace d’un langage de
spécification. Cela ne veut pas dire qu’un tel langage n’est pas pratique. Au contraire,
c’est un outil important pour réfléchir sur les programmes. On peut l’utiliser avec
un prouveur de théorèmes, qui est un programme qui peut faire certaines formes
de raisonnement mathématique. Les prouveurs de théorèmes pratiques ne sont pas
complètement automatiques ; ils ont besoin d’un coup de main humain. Mais ils
peuvent prendre sur eux une grande partie de la corvée du raisonnement sur les
programmes : la manipulation fastidieuse des formules mathématiques. Avec l’aide
d’un prouveur de théorèmes, un développeur peut souvent prouver des propriétés très
fortes de son programme. Une telle utilisation d’un prouveur de théorèmes s’appelle
l’ingénierie des preuves. Pour l’instant, l’ingénierie des preuves n’est pratique que
3. Si on n’utilise pas les possibilités non déclaratives de ces langages !
© Dunod – La photocopie non autorisée est un délit