J'ai mis en ligne un tutoriel à cette adresse : https://zestedesavoir.com/tutoriels/885/introduction-a-la-preuve-de-programmes-c-avec-frama-c-et-son-greffon-wp/ . Ce tutoriel concerne la preuve de programme écrits en langage C avec un logiciel qui s'appelle Frama-C. L'idée est d'introduire quelques notions à propos de la preuve, et de les appliquer dans le contexte d'un langage où elle est très utile car le langage nous donne peu de garanties : le C.
Pour ceux qui n'aiment pas les pages web, j'ai mis sur mon github une version PDF.
Je me permets un UP pour mentionner que le tutoriel est maintenant disponible en version finale (modulo les choses que j'ajouterai à l'avenir bien sûr ). C'est ici que ça se passe :
Impossible de télécharger le PDF il est introuvable et sur zeste de savoir j'ai le message "Vous n'avez pas les droits suffisants pour accéder à cette page."
J'ai survolé hier soir ton introduction. Je ne connaissais pas du tout et c'est assez intéressant mais je me demande si on peut prouver des fonctions un peu plus complexes qu'un min / max, qui renvoient du texte par exemple ?
Les deux exemples les plus complexes que j'aborde dans le tutoriel sont un algorithme de tri de tableau et la rechercher d'un sous tableau maximum dans un tableau. Donc oui, on peut faire plus complexe qu'un min/max mais je ne pense pas que ce soit la question .
Pour les fonctions qui renvoient du texte, ça va surtout dépendre de notre capacité à exprimer une spécification au sujet de ce texte et à abstraire son contenu, plus que la capacité des prouveurs en eux-mêmes. Après, les manipulations de texte sont assez notoirement connue pour être plus dures à prouver que pas mal d'autres propriétés. Des gens l'ont déjà fait avec le proveur interactif Coq : https://arxiv.org/abs/1105.2576 .
Pour ma part, j'ai utilisé Frama-C et WP pour vérifier que le module d'adressage virtuel d'un micronoyau respecte bien l'invariant "pour toute page de mémoire, le compteur présent dans sa structure de description est égal au nombre de fois où le numéro de cette page apparaît dans la mémoire" (grossièrement) y compris en présence de multi-threading. Donc, oui, on peut prouver des choses complexes avec Frama-C. D'autres études :
Pour information la version anglaise du tutoriel a subi une très grosse mise à jour récemment. Il est aujourd'hui en bêta et je vise à finaliser les derniers détails pour une sortie juste après la sortie de la prochaine release de Frama-C. La version PDF est disponible sur ce post sur ZDS. N'hésitez pas à y jeter un oeil pour m'apporter des retours.
La version française devrait suivre, mais cela va demander à mon avis quelques semaines de réaliser la traduction dans son entier.
Sont désormais toute au même niveau et à jour pour la version actuelle de Frama-C. Maintenant, il faut que je tienne le rythme des changements de versions de Frama-C.
× Après avoir cliqué sur "Répondre" vous serez invité à vous connecter pour que votre message soit publié.
× Attention, ce sujet est très ancien. Le déterrer n'est pas forcément approprié. Nous te conseillons de créer un nouveau sujet pour poser ta question.
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C
Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C