Le langage fonctionnant par effet de bords, il faut effectivement utiliser la logique de Hoare pour vérifier la correction des programmes écrits avec.
Cela étant, il me semble que Thomas voulait dire que l'exemple était monomorphe (les deux variables d'entrées sont de types Int) et non polymorphes (il n'y a pas de variable de types); d'où sa remarque sur le manque de généralité.
Quoi qu'il en soit, la logique de Hoare est une proche parente de la théorie des types en partageant le même fondement : la structure logico-déductive de l'ésprit humain. Par exemple, la règle de composition :
{P} S {Q} , {Q} T {R}
---------------------
{P} S; T {R}
est la version impérative du typage de la composition de fonction dans les langages fonctionnels (('p -> 'q) -> ('q -> 'r) -> 'p -> 'r dans le langage des types de OCaml), règle qui a pour fondement une double application du modus ponens (si A alors B, or A, donc B).
Les programmeurs impératifs composent les instructions, comme les programmeurs fonctionnels composent les fonctions.
P.S : Joli dépêche qui résume bien le domaine et l'état des lieux. J'étais passé à côté et je compte bien t'écrire un commentaire plus long et détaillé (qui me demandera plus de temps que cette simple remarque sur la logique de Haore). En plus, ça me permettra de parler de mes marottes (la logique formelle, la théorie de la démonstration, la correspondance de Curry-Howard et la philosophie des mathématiques) sans que thoasm m'en fasse le reproche. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada
Posté par kantien . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 3.
Le langage fonctionnant par effet de bords, il faut effectivement utiliser la logique de Hoare pour vérifier la correction des programmes écrits avec.
Cela étant, il me semble que Thomas voulait dire que l'exemple était monomorphe (les deux variables d'entrées sont de types
Int) et non polymorphes (il n'y a pas de variable de types); d'où sa remarque sur le manque de généralité.Quoi qu'il en soit, la logique de Hoare est une proche parente de la théorie des types en partageant le même fondement : la structure logico-déductive de l'ésprit humain. Par exemple, la règle de composition :
est la version impérative du typage de la composition de fonction dans les langages fonctionnels (
('p -> 'q) -> ('q -> 'r) -> 'p -> 'rdans le langage des types de OCaml), règle qui a pour fondement une double application du modus ponens (si A alors B, or A, donc B).Les programmeurs impératifs composent les instructions, comme les programmeurs fonctionnels composent les fonctions.
P.S : Joli dépêche qui résume bien le domaine et l'état des lieux. J'étais passé à côté et je compte bien t'écrire un commentaire plus long et détaillé (qui me demandera plus de temps que cette simple remarque sur la logique de Haore). En plus, ça me permettra de parler de mes marottes (la logique formelle, la théorie de la démonstration, la correspondance de Curry-Howard et la philosophie des mathématiques) sans que thoasm m'en fasse le reproche. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.