Bonjour les agrumes !
Correction du format des formules pour assurer la génération correcte en PDF.
Merci d’avance pour vos commentaires.
Merci pour le tutoriel très complet. Je suis en train de travailler là-dessus en cours, donc j’en profite pour te faire un retour de débutant.
Et d’autre part, il existe également des techniques permettant d’analyser les spécifications en quête d’erreurs ou de manquements.
Tu pourrais fournir des ressources à ce sujet, sous forme de mots-clés ou liens.
même s’il existe également des analyses dynamiques notamment en ce qui concerne le monitoring de code
Je pense qu’une note à ce propos serait la bienvenue pour expliquer un peu plus (mais brièvement quand même) ce dont il est question.
Ce modèle peut être plus ou moins abstrait selon la technique utilisée, c’est donc une approximation des états possibles de notre programme.
Il me semble judicieux d’ajouter un exemple illustrant la différence entre modèles abstraits et concrets. Ce serait d’ailleurs l’occasion d’aérer un peu cette introduction très textuelle. 
Cette écriture nous dit "si nous sommes dans un état où P est vrai, alors, après exécution de C et si C termine, alors Q sera vrai pour le nouvel état du programme". Dis autrement, P est la pré-condition nécessaire pour que C nous amène à la post-condition Q
Le "si… alors" désigne une condition suffisante et semble donc en contradiction avec le "pré-condition nécessaire".
Détail : tu as deux "alors" dans ta première phrase.
Calcul de plus faible pré-condition
Les deux exemples que tu donnes (en C et en logique de Hoare) me paraissent un peu simplistes. Peut-être pourrais-tu utiliser une fonction, avec un corps un peu plus complexe ? Je vais réfléchir à un exemple, mais un truc qui implique une division par zéro me semble intéressant.
Encore merci !
Lu’!
Et d’autre part, il existe également des techniques permettant d’analyser les spécifications en quête d’erreurs ou de manquements.
Tu pourrais fournir des ressources à ce sujet, sous forme de mots-clés ou liens.
même s’il existe également des analyses dynamiques notamment en ce qui concerne le monitoring de code
Je pense qu’une note à ce propos serait la bienvenue pour expliquer un peu plus (mais brièvement quand même) ce dont il est question.
Je vais en toucher deux mots.
Ce modèle peut être plus ou moins abstrait selon la technique utilisée, c’est donc une approximation des états possibles de notre programme.
Il me semble judicieux d’ajouter un exemple illustrant la différence entre modèles abstraits et concrets. Ce serait d’ailleurs l’occasion d’aérer un peu cette introduction très textuelle.
Ce ne sera peut être pas beaucoup moins textuel 
. Mais je vais voir ce que je peux faire 
.
Cette écriture nous dit "si nous sommes dans un état où P est vrai, alors, après exécution de C et si C termine, alors Q sera vrai pour le nouvel état du programme". Dis autrement, P est la pré-condition nécessaire pour que C nous amène à la post-condition Q
Le "si… alors" désigne une condition suffisante et semble donc en contradiction avec le "pré-condition nécessaire".
C’est vrai, je vais corriger ça.
Les deux exemples que tu donnes (en C et en logique de Hoare) me paraissent un peu simplistes. Peut-être pourrais-tu utiliser une fonction, avec un corps un peu plus complexe ? Je vais réfléchir à un exemple, mais un truc qui implique une division par zéro me semble intéressant.
Oui, c’était plutôt volontaire pour ne pas rentrer immédiatement dans le gras du sujet. Je vais voir ça. Sachant qu’introduire un exemple avec une division par 0, ça implique déjà de parler de vérification d’absence d’erreur à l’exécution, qui est légèrement déconnecté. Je vais voir.
Bonjour les agrumes !
La bêta a été mise à jour avec les remarques de @Vayel sauf :
Pour l’instant je n’ai pas d’idée sur ce point et je préfère rester très soft à ce sujet. En particulier, ne pas rentrer immédiatement sur la problématique d’erreur à l’exécution.
Merci d’avance pour vos commentaires.
Salut !
J’ai repris ma lecture :
Nous pouvons spécifier plusieurs post-conditions, soit en les composants avec un && comme en C, soit en introduisant une nouvelle clause ensures, comme illustré ci-dessous.
Je me suis demandé à quoi servait la première post-condition dans la mesure où elle était conséquence de la seconde. J’imagine que la façon de choisir les bonnes pré-conditions ne s’explique pas en début de tutoriel, mais peut-être pourrais-tu en toucher un mot (ne serait-ce que pour dire qu’on y reviendra plus tard et que ce n’est pas la peine de se casser la tête là-dessus maintenant).
La table de vérité de l’implication est la suivante
"0" et "1", voire "F" et "V", me semblent plus clairs que les symboles utilisés. Disons qu’il ne nécessite pas d’avoir déjà été manipulés pour être compris. Là, à chaque case, je dois retourner voir à quoi correspond le symbole.
Comme le montre cette capture d’écran, nous avons deux nouveaux codes couleur pour les pastilles : vert+marron et orange.
Malgré le TP que j’ai eu ce matin à ce sujet, j’ai toujours du mal à comprendre le sens de ces pastilles. Je pense que ça vaut le coût d’expliciter avec un exemple simple pour chacune. Notamment, que faut-il que je fasse concrètement quand je rencontre une de ces pastilles ?
La couleur vert + marron nous indique que la preuve a été effectué mais qu’elle dépend potentiellement de propriétés qui, elle, ne l’ont pas été. Si la preuve n’est pas recommencée
De ce que j’ai compris, la partie en gras concerne un détail d’utilisation du logiciel. Tu pourrais la séparer clairement (avec un retour à la ligne) de l’explication sur le sens de la pastille pour rendre cette dernière plus claire.
nous pouvons donc voir que les hypothèses n’ont pas suffi aux prouveurs pour déterminer que la propriété est vraie
Tu pourrais rappeler la propriété en question (absence de débordement) comme tu as digressé sur le fonctionnement des prouveurs.
La fenêtre de Frama-C ne permet pas l’édition du code source.
Je me demande s’il n’est pas préférable que ce message apparaisse avant. Certes, c’est la première fois que le lecteur est censé éditer le code source, mais s’il a voulu jouer avec avant, il aura été déçu de ne pas pouvoir modifier le texte.
Une fois le code source modifié de cette manière, un clic sur "Reparse"
Ce matin en TP, les profs nous disaient que "Reparse" était assez peu fiable et qu’il valait mieux quitter et réouvrir.
Nous pouvons également vérifier qu’une fonction qui appellerait abs respecte bien la pré-condition qu’elle impose :
C’est incroyable, en tant que daltonien, je ne vois absolument pas la différence entre les pastilles vertes et oranges. Ca vaudrait peut-être le coût de le faire remonter aux devs.
À partir de là, nous pouvons prouver tout ce que nous voulons car ce "false" devient une pré-condition pour tout appel qui viendrait ensuite.
J’ai buté sur le terme "pré-condition", parce que pour moi ça désigne une condition à respecter (et non "respectée") en entrée de fonction. En lisant cette phrase, j’ai eu l’impression qu’on avait en quelque sorte ajouté la ligne \requires false. Alors qu’en fait, si j’ai bien compris, c’est juste le contexte de preuve qui a changé.
Conséquence logique, l’appel suivant abs(a) reçoit dans ses suppositions "False".
Le terme "supposition" me semble bien plus adapté que le précédent "pré-condition". 
Par contre, nous aurons bien du mal à lui donner une valeur en entrée qui respecte la pré-condition, nous pourrons donc nous en apercevoir.
Je ne comprends pas la partie en gras. Frama-C fournit-il un outil pour ça ?
Encore merci pour le tutoriel.
(1) Je me suis demandé à quoi servait la première post-condition dans la mesure où elle était conséquence de la seconde. (2) J’imagine que la façon de choisir les bonnes pré-conditions ne s’explique pas en début de tutoriel, mais peut-être pourrais-tu en toucher un mot (ne serait-ce que pour dire qu’on y reviendra plus tard et que ce n’est pas la peine de se casser la tête là-dessus maintenant).
(1) C’est pour illustrer principalement, cela permet aussi d’avoir une connaissance plus simple que la propriété d’origine explicitée comme une formule directe et non déduite.
(2) Je peux en mettre deux mots, mais vraiment deux mots.
"0" et "1", voire "F" et "V", me semblent plus clairs que les symboles utilisés. Disons qu’il ne nécessite pas d’avoir déjà été manipulés pour être compris. Là, à chaque case, je dois retourner voir à quoi correspond le symbole.
OK.
Malgré le TP que j’ai eu ce matin à ce sujet, j’ai toujours du mal à comprendre le sens de ces pastilles. Je pense que ça vaut le coût d’expliciter avec un exemple simple pour chacune. Notamment, que faut-il que je fasse concrètement quand je rencontre une de ces pastilles ?
Je vais expliciter plus. Par contre le "que faut-il que je fasse", ça revient un peu à la question de @Taurre à ce sujet, et la réponse est "ce n’est pas évident car les prouveurs donnnent très peu d’infos".
De ce que j’ai compris, la partie en gras concerne un détail d’utilisation du logiciel. Tu pourrais la séparer clairement (avec un retour à la ligne) de l’explication sur le sens de la pastille pour rendre cette dernière plus claire. […] Tu pourrais rappeler la propriété en question (absence de débordement) comme tu as digressé sur le fonctionnement des prouveurs.
OK.
Je me demande s’il n’est pas préférable que ce message apparaisse avant. Certes, c’est la première fois que le lecteur est censé éditer le code source, mais s’il a voulu jouer avec avant, il aura été déçu de ne pas pouvoir modifier le texte.
Je vais déplacer ça dans la première fenêtre d’intro.
Ce matin en TP, les profs nous disaient que "Reparse" était assez peu fiable et qu’il valait mieux quitter et réouvrir.
Il y a pas une version antédiluvienne à ton école par hasard ? J’ai pas eu de problèmes depuis quelques versions avec Reparse (tiens par curiosité tu fais ça où et avec qui ?).
C’est incroyable, en tant que daltonien, je ne vois absolument pas la différence entre les pastilles vertes et oranges. Ca vaudrait peut-être le coût de le faire remonter aux devs.
Cela a déjà été remonté, j’ai rajouter aussi quelque chose dans l’intro pour ça. Tu peux lancer avec l’option suivante pour avoir un frama-c en mode daltonien :
1 | $ frama-c-gui -gui-theme colorblind |
J’ai buté sur le terme "pré-condition", parce que pour moi ça désigne une condition à respecter (et non "respectée") en entrée de fonction. En lisant cette phrase, j’ai eu l’impression qu’on avait en quelque sorte ajouté la ligne
\requires false. Alors qu’en fait, si j’ai bien compris, c’est juste le contexte de preuve qui a changé.[…]
Le terme "supposition" me semble bien plus adapté que le précédent "pré-condition".
Il faut que je le relise plus en détail. Mais de mémoire, au niveau du soft, ça devient bien une pré-condition des instructions qui suivent (cela vient de la notion de la règle de séquence d’instructions en logique de Hoare).
Je ne comprends pas la partie en gras. Frama-C fournit-il un outil pour ça ?
Tu pourrais exécuter value pour qu’il te dise qu’il n’y a aucune valeur qui marche. Mais l’idée est surtout que l’on ne pourra jamais prouver le code appelant et qu’en relisant on pourra s’apercevoir qu’on n’est pas très malin avec notre propriété.
Je mets à jour le premier post avec les évolutions à réaliser.
Il y a pas une version antédiluvienne à ton école par hasard ? J’ai pas eu de problèmes depuis quelques versions avec Reparse (tiens par curiosité tu fais ça où et avec qui ?).
Nous travaillons avec la version Aluminium-20160501.
Je suis étudiant à l’Ensimag. Nos profs sont des chercheurs au labo Verimag.
Tu peux lancer avec l’option suivante pour avoir un frama-c en mode daltonien :
Ca va me changer la vie, merci !
Il faut que je le relise plus en détail. Mais de mémoire, au niveau du soft, ça devient bien une pré-condition des instructions qui suivent (cela vient de la notion de la règle de séquence d’instructions en logique de Hoare).
C’est un peu bizarre comme terminologie parce que pour moi une pré-condition c’est une condition à vérifier. Du coup ce serait étrange qu’on doive vérifier le faux. A moins que je me trompe et que "pré-condition" signifie simplement "condition vérifiée avant le traitement" ?
Nous travaillons avec la version
Aluminium-20160501.Je suis étudiant à l’Ensimag. Nos profs sont des chercheurs au labo Verimag.
Ok, normalement, il n’est pas sensé y avoir de problèmes avec celle-ci et ultérieures. Donc à voir.
C’est un peu bizarre comme terminologie parce que pour moi une pré-condition c’est une condition à vérifier. Du coup ce serait étrange qu’on doive vérifier le faux. A moins que je me trompe et que "pré-condition" signifie simplement "condition vérifiée avant le traitement" ?
Oui et non. Pour plusieurs raisons. D’abord, en WP, tu ne vérifies pas la pré-condition au sens propre. Tu vérifies que la pré-condition donnée est plus forte que la pré-condition calculée.
Ensuite, dans un triplet $\{P\} prog \{Q\}$, $prog$ peut tout à fait être un programme partiel (et de fait, pendant le calcul, il le devient par les instructions successives). Et ce triplet signifie bien "si $P$ est vérifiée avant l’exécution de $prog$ et si elle termine alors $Q$ est vérifiée après". Donc dans le programme, on peut tout à fait mentionner un triplet $\{P\} c_1; c_2 \{Q\}$, même si des instructions précèdent $c_1$, et en cela $P$ est bien une pré-condition de la suite d’instruction.
Finalement, WP triche un peu, il ne fait pas du vrai calcul de plus faibles pré-conditions, il fait aussi des passes d’analyses avant pour raffiner les formules obtenues. Mais je ne vais pas rentrer dans de tels détails (je ne les connais d’ailleurs que très peu).
Salut !
Je poursuis ma relecture :
RAS
Pour comprendre ce que font précisément complete et disjoint, il est utile d’expérimenter deux possibilités :
Je me demande s’il ne serait pas intéressant de décrire le comportement de ces deux clauses. Je n’ai pas expérimenté mais j’imagine que le résultat est clair, toutefois il peut être judicieux de lever toute ambiguïté.
RAS
J’ai rajouté le point sur les comportements. Je viens de m’apercevoir que j’ai pété pleins de trucs dans des vieilles corrections. J’ai du avoir un cafouillage de versions quelque part. Donc pas mal de corrections pour la prochaine version à venir …
Bonjour les agrumes !
Finalement, j’ai enfin pu trouver du temps et la bêta a été mise à jour et décante sa pulpe à l’adresse suivante :
Au programme, réparation de corrections que j’avais cassées, corrections de la plupart des points soulevés par @Vayel. Sauf la question des complete/disjoint parce que je ne comprends finalement pas ce qui manque dans l’explication qui précède la question "expérimentation".
J’ai également pour projet de faire rentrer le type "list" dans les prochaines versions, mais il faut encore que je l’expérimente un peu plus. Je mettrais le PDF de mon github à jour bientôt et je mettrais un lien vers celui-ci dans le post principal.
Merci d’avance pour vos commentaires.
J’ai mis un lien vers une version PDF. Pendant le portage en PDF j’ai détecté quelques erreurs supplémentaires, mais elles vont attendre un peu.
Bonjour les agrumes !
En fait j’ai trouvé du temps, donc quelques typos ont été corrigées. J’aimerai bien avoir une relecture supplémentaire sur les 3 dernières parties avant de proposer en validation. Et des infos sur le point soulevé par @Vayel pour les comportements.
Merci d’avance pour vos commentaires.
Bon j’ai moi même relu les dernières parties à la recherche de nouvelles coquilles et ça me semble pas mal. Donc je mets en demande de validation et advienne que bourrin.
Bonjour les agrumes !
La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :
Merci d’avance pour vos commentaires.
Bonjour,
La bêta du contenu « Introduction à la preuve de programmes C avec Frama-C et son greffon WP » a été désactivée.
Les prochains changement viendront avec une durée indéterminée. Au programme :
.
Oyez oyez les agrumes !
Je vous annonce avec plaisir la ré-ouverture de la bêta du contenu « Introduction à la preuve de programmes C avec Frama-C et son greffon WP » ! Je vous souhaite une agréable lecture à l’adresse suivante :
Pour l’instant rien de neuf dans la bêta actuelle. Je rouvre la bêta pour éviter de créer un nouveau sujet et pour garder un suivi centralisé de ce qui a été fait autour du tutoriel. Cependant, il y a eu quand même pas mal de travaux autour du tutoriel ces derniers mois, notamment sa traduction en anglais (je remercie au passage Jens Gerlach, ingénieur chercheur au Fraunhofer pour le temps qu’il y a consacré).
Cependant, tout n’a pas été relu, et mon anglais n’est pas des meilleurs donc si vous avez du temps à consacrer à la relecture de la version anglaise, mon github y est ouvert (oui le nom est en français, je ne pensais pas qu’on manifesterait si vite un intérêt pour le traduire).
Dans les prochains mois, je vais sûrement migrer l’ensemble vers TeX pour faciliter la génération PDF et éviter de dupliquer les codes (tout en ayant ce qu’il faut pour générer du MD). La bonne nouvelle dans tout ça, c’est que je discute en ce moment avec Jens des ajouts que je pourrais faire à propos du contenu et donc que les ajouts de contenus vont pouvoir reprendre
Merci pour votre participation, on se tient au jus.
Pour info, je devrais ressortir le tutoriel du placard dans les semaines à venir (j’espère pour la prochaine release de Frama-C). Beaucoup de choses sont déjà disponibles sur la version anglaise (voir premier post du topic).
Pour cette version, je suis repassé à LaTeX qui me donne des outils plus confortables pour la présentation, et le code, en particulier du fait que je doive gérer versions anglaises et françaises. Pour l’instant tout le boulot a été effectué sur la version anglaise. Quand elle sera complète j’attaquerai la traduction vers la version française latex. Et après, je verrais pour ramener les changements vers la version markdown (avec pandoc, ça devrait être à peu près gérable).
Oyez ! Oh yeah !
Une version bêta du tutoriel dans sa version anglaise est maintenant disponible ici : version EN. Après plus d’un an de travail, voici les modifications réalisées:
Faisant passer le PDF de 90 pages dans sa version anglaise précédente à plus de 190 aujourd’hui.
Cette version va rester quelques temps en bêta, le temps que j’obtienne quelques retours à son sujet. N’hésitez pas à y participer ! Après cela le travail de traduction vers la version française commenceras.
Voilà ! Des bisous !
Salut,
J’ai commencé à apprendre Frama-C avec ton tutoriel et j’en profite pour le bêta-tester.
Si ça peut t’aider à me situer par rapport à ta cible, j’utilise Linux au quotidien depuis près de 10 ans, je suis un développeur amateur qui a touché à des langages divers (C, OCaml, Java, Python, essentiellement) avec pas mal de culture générale sur les écosystèmes des différents langages, et je connais un peu Coq et ai aussi pas mal de culture générale sur les méthodes formelles.
L’anglais est un peu étrange par endroit, mais ce n’est pas bloquant (et pas primordial).
Le premier gros écueil que j’ai eu, c’est l’installation. Il y a des instructions, ce qui est déjà bien, par contre, elles ne sont pas assez précises pour être autre chose que des indications. Je me doute bien que le mieux est de lire des instructions officielles quelque part, mais autant ne rien mettre dans le tutoriel et renvoyer vers la doc officielle si elle tient la route.
J’ai commencé par choisir la méthode utilisant le gestionnaire du paquet du système (Linux Mint pour ma part). J’ai eu un mal fou à trouver le vrai nom des paquets pour les installer, ce qui n’était pas très pratique. Ensuite, sans surprise, la version des dépôts était ancienne et ne se ressemblait pas assez au tuto pour suivre correctement. J’ai donc décidé de faire la méthode d’installation avec OPAM.
Avec OPAM, j’ai pu installer ce qu’il faut, mais j’ai vraiment galéré (en partie à cause de mon inexpérience avec l’outil) :
Bref, cette étape a été un peu frustrante.
Le PDF ne me permet pas de copier-coller correctement. Pour le code de test de l’installation, ce n’est pas très pratique ; j’ai dû ajuster à la main. Ça se fait, mais c’est désagréable.
Plus loin, on dit que l’implication est équivalent à ¬A∧B, ce qui est faux, puisque c’est (NON A) OU B.
C’est sympa de voir que Z3 dépasse le temps alloué, mais je ne vais pas installer Z3 au tout début du tuto juste pour ça. Et ça fait que je me demande un peu si je devrais avoir Z3 moi aussi à ce stade ou pas.
Je me demande si le vocabulaire ne devrait pas être plus cohérent avec l’interface. Je vois que tu utilises beaucoup "verification conditions", mais l’interface parle de "goals" (dans l’onglet) ou de "proof obligations" (quand on en supprime une avec "Clear").
Après je crois que tu n’y peux rien, mais si j’insère un caractère étrange dans un fichier (par exemple une espace insécable), ça produit une entrée invalide pour Frama-C (normal), mais si je corrige le fichier, alors Frama-C me sort un message d’erreur pour ce fichier et tous les autres fichiers que j’essaie de charger ! J’ai été obligé de relancer Frama-C pour faire disparaître le problème. J’imagine que c’est un bug, mais c’est carrément grossier. J’utilise la version "Frama-C 18.0 (Argon)". On va où pour faire des rapports de bugs ?
L’exercice 3 sur l’alphabet est un peu bizarre dans le PDF, vu qu’on attend explicitement 1 et 0 pour r. Par contre, sur le dépôt on utilise bien r comme un booléen. J’ai du mal à savoir lequel est le plus récent à cause des dates.
L’exemple de la division (3.2.4.1) est plus délicat qu’il n’y paraît. Il y a une page Wikipédia entière qui parle de ça. En gros, le code de correction actuel manque une post-condition et si on prend la définition traditionnelle, alors le code est problématique. Je crois que c’est un exemple à éviter, si on veut rester simple.
Provide a contract for the following function that reset its first parameter if the second is true
if and only if
Bon c’est tout pour aujourd’hui.
L’anglais est un peu étrange par endroit, mais ce n’est pas bloquant (et pas primordial).
Hésite pas à juste faire une marque quelque part pour me signaler les points où c’est moche.
Le premier gros écueil que j’ai eu, c’est l’installation. Il y a des instructions, ce qui est déjà bien, par contre, elles ne sont pas assez précises pour être autre chose que des indications. Je me doute bien que le mieux est de lire des instructions officielles quelque part, mais autant ne rien mettre dans le tutoriel et renvoyer vers la doc officielle si elle tient la route.
OK, je peux travailler là dessus.
J’ai commencé par choisir la méthode utilisant le gestionnaire du paquet du système (Linux Mint pour ma part). J’ai eu un mal fou à trouver le vrai nom des paquets pour les installer, ce qui n’était pas très pratique. Ensuite, sans surprise, la version des dépôts était ancienne et ne se ressemblait pas assez au tuto pour suivre correctement. J’ai donc décidé de faire la méthode d’installation avec OPAM.
OK, donc la situation de ce côté est de pire en pire. Je note. J’hésite de plus en plus à virer les éléments liés aux gestionnaires de paquets. Personne ne veut faire ces paquets. C’est pénibles, il y a 50 gestionnaires et chacun a ses règles pour faire entrer un paquet …
- plein d’erreurs de compilation pour des histoires de dépendance externes (dont autoconf que je n’avais pas et qui n’est pas listé dans le tuto je crois) ;
- histoires de dépendance internes (sachant que les messages d’erreur ne sont pas toujours très clair), que j’ai réglé avec update/upgrade dans opam (sérieux ? Ce n’est pas le boulot d’opam de vérifier que j’ai les bonnes versions ?!) ;
- après, j’ai pas pigé tout de suite que l’environnement était mal configuré et que c’était pour ça que j’ouvrais l’ancienne version.
Autoconf a été ajouté relativement récemment c’est vrai. Il faut que je rajoute ça. Je me demande s’il y a pas m4 maintenant que tu le dis. Pour les dépendances internes si c’est la version en cours (et pas potassium qui arrive très bientôt), oui il y a eu des soucis qui sont possiblement pas tous encore réglés c’est pour ça que j’ai visé potassium d’ailleurs. (Edit: partially Done)
Le PDF ne me permet pas de copier-coller correctement. Pour le code de test de l’installation, ce n’est pas très pratique ; j’ai dû ajuster à la main. Ça se fait, mais c’est désagréable.
Hum. Tu pourrais remonter directement sur le repo de zmarkdown ? Parce que je me base complètement dessus et s’il y a le problème sur mon tuto, il n’est pas exclus que le problème soit aussi présent sur les PDF de ZDS. Et perso j’ai moyennement les compétences pour comprendre ce qui merde et pourquoi du côté de LaTeX 
.
Plus loin, on dit que l’implication est équivalent à ¬A∧B, ce qui est faux, puisque c’est
(NON A) OU B.
Thanks, faute de frappe. (EDIT: Done)
C’est sympa de voir que Z3 dépasse le temps alloué, mais je ne vais pas installer Z3 au tout début du tuto juste pour ça. Et ça fait que je me demande un peu si je devrais avoir Z3 moi aussi à ce stade ou pas.
OK, je vais remettre un passage pour expliquer qu’ici ce n’est pas nécessaire. Mais plus on avance vers la fin du tutoriel, plus les solveurs autres peuvent devenir intéressantes. J’ai mis deux trois exemples au fil du tutoriel qui expliquent cela, mais il n’est pas fondamentalement nécessaire d’avoir Z3 pour juste prendre l’info en question. Par contre, pour vraiment faire de la preuve sur de vrais programmes, il est peu probable qu’un seul solveur suffise.
(EDIT: Done)
Je me demande si le vocabulaire ne devrait pas être plus cohérent avec l’interface. Je vois que tu utilises beaucoup "verification conditions", mais l’interface parle de "goals" (dans l’onglet) ou de "proof obligations" (quand on en supprime une avec "Clear").
Le truc c’est que le terme "verification condition" est le terme idoine normalement.
Après je crois que tu n’y peux rien, mais si j’insère un caractère étrange dans un fichier (par exemple une espace insécable), ça produit une entrée invalide pour Frama-C (normal), mais si je corrige le fichier, alors Frama-C me sort un message d’erreur pour ce fichier et tous les autres fichiers que j’essaie de charger ! J’ai été obligé de relancer Frama-C pour faire disparaître le problème. J’imagine que c’est un bug, mais c’est carrément grossier. J’utilise la version "Frama-C 18.0 (Argon)". On va où pour faire des rapports de bugs ?
Il y a le BTS de Frama-C (https://bts.frama-c.com/my_view_page.php). L’interface graphique est l’un des trucs les plus vieux de Frama-C. Et il y a quelques bugs de ce genre. A ma connaissance, elle doit être changée d’ici ou une ou deux versions, ce qui explique pourquoi l’ancienne GUI ne reçoit que peu d’amélioration.
L’exercice 3 sur l’alphabet est un peu bizarre dans le PDF, vu qu’on attend explicitement 1 et 0 pour r. Par contre, sur le dépôt on utilise bien r comme un booléen. J’ai du mal à savoir lequel est le plus récent à cause des dates.
Je vais check ça. (EDIT: Done)
L’exemple de la division (3.2.4.1) est plus délicat qu’il n’y paraît. Il y a une page Wikipédia entière qui parle de ça. En gros, le code de correction actuel manque une post-condition et si on prend la définition traditionnelle, alors le code est problématique. Je crois que c’est un exemple à éviter, si on veut rester simple.
OK, je vais regarder ça de plus près et essayer de trouver un autre exemple. Ou peut être changer les types, ça pourrait être suffisant pour régler le problème. (EDIT: Done -> unsigned)
Provide a contract for the following function that reset its first parameter if the second is true
if and only if
Noté. (EDIT: Done)
Bon c’est tout pour aujourd’hui.
Merci
@Aabu : Pour la partie installation par les dépôts tu te souviens des noms des paquets pour lesquels ça a vraiment posé problème ? Alt-ergo, why3, Frama-C ?
(Sinon, j’ai trouvé une mise à jour de la doc qui indique un package Opam qui peut traiter les dépendances externes visiblement).
Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte