“doc” (Col. : Science Sup 17x24) — 2007/7/19 — 18:18 — page 10 — #20
i
i
i
i
i
i
i
i
10
1
• Introduction aux concepts de programmation
1.6 L’EXACTITUDE
Un programme est correct (« exact ») s’il fait ce que nous voulons qu’il fasse. Comment peut-on s’assurer qu’un programme est correct ? Dans la plupart des cas il est
impossible de refaire manuellement les calculs du programme. Il nous faut d’autres
techniques. Une technique simple, que nous avons déjà utilisée, est de vérifier que le
programme est correct pour les résultats que nous connaissons. Cela augmente notre
confiance dans le programme. Mais cela ne va pas très loin. Pour prouver l’exactitude
de façon sûre, il faut raisonner sur le programme. Cela signifie trois choses :
– Nous avons besoin d’un modèle mathématique des opérations du langage de
programmation qui définit ce qu’elles font. Ce modèle s’appelle la sémantique
du langage.
– Nous devons définir ce que nous voulons que le programme fasse. C’est une
définition mathématique des entrées dont le programme a besoin et des résultats
qu’il calcule. Cela s’appelle la spécification du programme.
– Nous utilisons des techniques mathématiques pour raisonner sur le programme en
utilisant la sémantique du langage. Nous voudrions démontrer que le programme
satisfait la spécification.
Un programme que l’on a prouvé correct pourra toujours donner de faux résultats
si le système sur lequel il s’exécute est mal implémenté. Comment pouvons-nous
être sûr que le système satisfait la sémantique ? La vérification d’un système est
une tâche lourde : il faut vérifier le compilateur, le système d’exécution, le système
d’exploitation, le matériel et la physique sur laquelle est basée le matériel ! Toutes ces
tâches sont importantes, mais elles sont hors de notre portée.
3
L’induction mathématique
Une technique utile pour raisonner sur un programme est l’induction mathématique.
Cette technique se compose de deux étapes. D’abord, nous démontrons que le programme est correct pour le cas le plus simple de l’entrée. Ensuite, nous démontrons
que, si le programme est correct pour un cas donné, il sera correct pour le cas suivant.
Si nous sommes sûrs que tous les cas seront traités tôt ou tard, alors l’induction mathématique nous permettra de conclure que le programme est toujours correct. On peut
appliquer cette technique aux entiers et aux listes :
– Pour les entiers, le cas le plus simple est 0 et pour un entier donné n le cas suivant
est n + 1.
3. Certains, en s’inspirant des paroles de Thomas Jefferson, diront que le prix de l’exactitude est la
vigilance éternelle.
i
i
i
i
i
i
i
i
10
1
• Introduction aux concepts de programmation
1.6 L’EXACTITUDE
Un programme est correct (« exact ») s’il fait ce que nous voulons qu’il fasse. Comment peut-on s’assurer qu’un programme est correct ? Dans la plupart des cas il est
impossible de refaire manuellement les calculs du programme. Il nous faut d’autres
techniques. Une technique simple, que nous avons déjà utilisée, est de vérifier que le
programme est correct pour les résultats que nous connaissons. Cela augmente notre
confiance dans le programme. Mais cela ne va pas très loin. Pour prouver l’exactitude
de façon sûre, il faut raisonner sur le programme. Cela signifie trois choses :
– Nous avons besoin d’un modèle mathématique des opérations du langage de
programmation qui définit ce qu’elles font. Ce modèle s’appelle la sémantique
du langage.
– Nous devons définir ce que nous voulons que le programme fasse. C’est une
définition mathématique des entrées dont le programme a besoin et des résultats
qu’il calcule. Cela s’appelle la spécification du programme.
– Nous utilisons des techniques mathématiques pour raisonner sur le programme en
utilisant la sémantique du langage. Nous voudrions démontrer que le programme
satisfait la spécification.
Un programme que l’on a prouvé correct pourra toujours donner de faux résultats
si le système sur lequel il s’exécute est mal implémenté. Comment pouvons-nous
être sûr que le système satisfait la sémantique ? La vérification d’un système est
une tâche lourde : il faut vérifier le compilateur, le système d’exécution, le système
d’exploitation, le matériel et la physique sur laquelle est basée le matériel ! Toutes ces
tâches sont importantes, mais elles sont hors de notre portée.
3
L’induction mathématique
Une technique utile pour raisonner sur un programme est l’induction mathématique.
Cette technique se compose de deux étapes. D’abord, nous démontrons que le programme est correct pour le cas le plus simple de l’entrée. Ensuite, nous démontrons
que, si le programme est correct pour un cas donné, il sera correct pour le cas suivant.
Si nous sommes sûrs que tous les cas seront traités tôt ou tard, alors l’induction mathématique nous permettra de conclure que le programme est toujours correct. On peut
appliquer cette technique aux entiers et aux listes :
– Pour les entiers, le cas le plus simple est 0 et pour un entier donné n le cas suivant
est n + 1.
3. Certains, en s’inspirant des paroles de Thomas Jefferson, diront que le prix de l’exactitude est la
vigilance éternelle.