@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).
@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 ?
Malheureusement, je ne me souviens pas. Pour être sûr de son coup, il faudrait faire des tests dans une VM sur un système vierge.
J’ai continué un peu ma lecture.
Les exercices sur les behaviors (3.3.1) sont assez ennuyeux et je n’ai pas eu le courage de tous les faire. Surtout qu’on reprend ceux d’avant… J’ai trouvé qu’ils sont assez artificiels, surtout celui où on dit d’enlever des trucs et d’en rajouter pour faire réussir/échouer la preuve de complétude ou disjonction. Autant quand on passe dessus la première fois, on se dit « c’est pour apprendre », autant la seconde fois, c’est un peu la corvée.
Celui qui semble le moins gavant est celui avec les catégories de caractères (3.4.1.2), mais il reste un peu artificiel.
De ce que je comprends, un des intérêts majeurs des behaviors par rapport à un ensemble d’implications, c’est la possibilité de vérifier qu’ils sont complets ou disjoints. Tu en parles bien sûr, mais j’ai l’impression que tu pourrais mettre plus en valeur ça. Tu parles de déterminisme à un endroit, ce n’est pas vraiment illustré dans les exercices. La complétude est illustrée, mais pas forcément sur des cas non-triviaux.
Je pense qu’un exercice un peu plus élaboré aurait sa place, mais demande de créer un peu de contexte. Quelque chose du genre ci-dessous (que j’ai inventé à l’arrache avec un bout de code).
Dans un premier temps, on imagine une machine avec trois modes (off, idle, operating) et un interrupteur (on, off). Le besoin est le suivant :
- si l’interrupteur est off, on doit éteindre la machine (mode == off) ;
sinon, si l’interrupteur est on,
- quand on est éteint, on passe en idle ;
- quand on est idle, on passe en operating ;
- quand on est operating, on reste operating.
Dans un second temps, on rajoute un watchdog pour assurer la sûreté de fonctionnement :
- si le watchdog détecte une erreur, alors la machine ne doit pas être operating.
/* Machine state */
enum MS {
MS_OFF, MS_IDLE, MS_OPERATING,
};
/* Switch state */
enum SS {
SS_OFF, SS_ON,
};
/* Watchdog state */
enum WS {
WS_OK, WS_ERROR,
};
/*@
requires ms \in {MS_OFF, MS_IDLE, MS_OPERATING};
requires ss \in {SS_OFF, SS_ON};
requires ws \in {WS_OK, WS_ERROR};
ensures \result \in {MS_OFF, MS_IDLE, MS_OPERATING};
behavior safety:
assumes ws == WS_ERROR;
ensures \result != MS_OPERATING;
behavior switch_off:
assumes ss == SS_OFF;
ensures \result == MS_OFF;
behavior switch_on:
assumes ms == MS_OFF && ss == SS_ON;
ensures \result == MS_IDLE;
behavior start_operating:
assumes ms == MS_IDLE && ss == SS_ON;
ensures ws != WS_ERROR ==> \result == MS_OPERATING;
behavior continue_operating:
assumes ms == MS_OPERATING && ss == SS_ON;
ensures ws != WS_ERROR ==> \result == MS_OPERATING;
complete behaviors;
disjoint behaviors switch_off, switch_on, start_operating, continue_operating;
*/
int transition(int ms, int ss, int ws) {
if (ms == MS_OFF) {
if (ss == SS_OFF)
return MS_OFF;
else
return MS_IDLE;
}
else if(ms == MS_IDLE) {
if (ss == SS_OFF || ws == WS_ERROR)
return MS_OFF;
else
return MS_OPERATING;
}
else {
if (ss == SS_OFF || ws == WS_ERROR)
return MS_OFF;
else
return MS_OPERATING;
}
}
int main() {
int ms = MS_OPERATING;
int ss = SS_ON;
int ws = WS_OK;
ms = transition(ms, ws, ws);
//@ assert ws == WS_ERROR ==> ms != MS_OPERATING;
ws = WS_ERROR;
ms = transition(ms, ws, ws);
//@ assert ws == WS_ERROR ==> ms != MS_OPERATING;
return 0;
}
Quand j’ai essayé d’inventer/résoudre l’exercice, je me suis rendu compte des trucs suivants.
Bref, c’était improvisé, mais assez formateur finalement. Je suis parti un peu loin. 
Finally, we can ask WP to verify that behaviors are disjoint (to guarantee determinism)
Du coup, j’ai une question. Pourquoi tu parles de déterminisme dans ce cas-là ? Parce qu’au pire, on a des post-conditions contradictoires, mais je vois pas en quoi c’est non déterminste. Et tu as des cas d’usages réalistes ou on a vraiment besoin de cas non-disjoints ? Dans mon exemple, j’ai fait ça de manière un peu tordue pour tester la complétude…
Merci pour ton retour, je regarderai ça de plus près après mes vacances.
Les exercices sur les behaviors (3.3.1) sont assez ennuyeux et je n’ai pas eu le courage de tous les faire. Surtout qu’on reprend ceux d’avant… J’ai trouvé qu’ils sont assez artificiels, surtout celui où on dit d’enlever des trucs et d’en rajouter pour faire réussir/échouer la preuve de complétude ou disjonction. Autant quand on passe dessus la première fois, on se dit « c’est pour apprendre », autant la seconde fois, c’est un peu la corvée.
Certes. Mais à ce stade du tutoriel, on n’a pas eu énormément de matière pour produire de nouveaux exercices. Et il est facile d’avoir des exercices qui deviennent rapidement trop complexes pour débuter (amha). Tu l’as d’ailleurs vu avec l’exercice que tu as écris qui devient rapidement très compliqué.
De ce que je comprends, un des intérêts majeurs des behaviors par rapport à un ensemble d’implications, c’est la possibilité de vérifier qu’ils sont complets ou disjoints. Tu en parles bien sûr, mais j’ai l’impression que tu pourrais mettre plus en valeur ça. Tu parles de déterminisme à un endroit, ce n’est pas vraiment illustré dans les exercices. La complétude est illustrée, mais pas forcément sur des cas non-triviaux.
Je vais essayer d’y réfléchir mais je ne veux pas arriver au degré de complexité de ton exemple.
- Ce n’est pas tout à fait évident d’écrire la spécifications en terme de behaviors, parce qu’il y a plusieurs variables d’entrées qui peuvent prendre différentes valeurs et donc plusieurs choix de behaviors cohérents possibles.
Normalement, la spec est justement là pour que le comportement soit clairement défini.
Finally, we can ask WP to verify that behaviors are disjoint (to guarantee determinism)
(1) Du coup, j’ai une question. Pourquoi tu parles de déterminisme dans ce cas-là ? (2) Parce qu’au pire, on a des post-conditions contradictoires, mais je vois pas en quoi c’est non déterminste. (3) Et tu as des cas d’usages réalistes ou on a vraiment besoin de cas non-disjoints ? Dans mon exemple, j’ai fait ça de manière un peu tordue pour tester la complétude…
(1) C’est une formulation qui vient entre autre des normes type DO-178 qui te disent que lorsque tu définis les scénarios d’usage d’une fonction, tu dois être sûr qu’un seul des scénarios est valable. Si tu ne peux pas identifier cet unique scénario dans une spécification, c’est considéré comme un trop grand risque.
(2) Ce pire cas, est clairement le pire qui peut t’arriver dans un programme. Heureusement, tu ne devrais pas être capable de prouver un tel scénario normalement. Et pour le non déterminisme, voir 1.
(3) Oui, mais c’est quelque chose que j’ai encore insuffisamment exploré pour l’expliquer dans une partie du cours. Ici, on sort de la partie requirements pour entrer plus dans de l’ingénierie de la preuve. En gros, on peut avoir des scénarios joints que l’on utilise pour prouver différentes propriétés qui sont plus faciles à prouver en changeant la manière dont les behaviors sont définis, et on utilise divers mots clés pour guider la preuve sur ces différents sets de behaviors. Par exemple, on pourrait imaginer avoir un ensemble de behaviors qui expriment le comportement fonctionnel de la fonction et un autre ensemble, joint au premier où l’on spécifie plutôt ce qui a trait à l’absence de runtime errors, et les behaviors pourraient ne pas avoir de correspondance d’un set à l’autre.
Je vais encore être un peu lent à répondre pendant quelques temps, je commence un nouveau job donc j’ai un peu de boulot pour me mettre en place.
we define the assignment of a memory location as an update of the memory suchthat now the corresponding pointer points to the written expression
Tu as écris = au lieu de := pour cette définition de weakest precondition.
4.2.6.4. Early termination
Frama-C m’a relevé une erreur [kernel:annot-error] loop_invar.c:28: Warning: unbound logic variable i. Ignoring code annotation. En déclarant i en dehors de la boucle, ça marche.
4.3.3.1. Non-mutating: Forall, Exists, ..
Dans cet exercice, je n’ai pas trouvé comment réutiliser le contrat de pred pour définir les autres fonctions. Je voulais écrire quelque chose du genre :
/*@
requires \valid_read(a + (0 .. s - 1));
assigns \nothing;
ensures \result <==> \forall size_t i; 0 <= i < s ==> pred(a[i]);
*/
int forall_pred(int* a, size_t s)
mais je n’ai pas abouti. J’ai fini par virer pred et considérer les valeurs comme des booléens.
En regardant un peu plus loin, j’ai l’impression qu’il faudrait définir un prédicat et le réutiliser pour les autres fonctions, c’est bien ça ? Si oui, je me demande si cet exercice n’aurait pas plutôt sa place plus loin, quitte à garder une version sans pred ici.
J’ai essentiellement survolé le reste (je me suis arrêté à la fin de la partie 4), je ne pense pas que j’irai plus loin. En tout cas, pas pour l’instant.
J’ai l’impression que les autres parties sont clairement un approfondissement (même si ça reste une "introduction" selon le sens académique du terme). Je me demande même si ça ne vaudrait pas le coup de faire deux documents/parties/tomes :
Et si ça grossit encore, faire quelque chose à la Software Foundations avec des parcours, les fondamentaux formant à mon avis un tronc commun.
Je pense relire un peu l’anglais, au moins pour les premiers chapitres (ceux que j’ai lus !), parce que j’y ai vu quelques erreurs et étrangetés. Par contre, ce n’est pas du tout ma langue maternelle et si tu veux atteindre une qualité supérieure de la langue, il faudra un relecteur natif.
Il me semblait avoir répondu à ce message mais en fait pas du tout. Désolé @Aabu 
.
Je devrais pouvoir me remettre sur la rédaction/correction d’éléments du tutoriel d’ici peu. Espérons avant que la prochaine version de Frama-C sorte. Hormis les points "simples" que je reprendrais lorsque je m’y attaquerait, juste quelques éléments de réponse pour les deux points suivants:
Frama-C m’a relevé une erreur
[kernel:annot-error] loop_invar.c:28: Warning: unbound logic variable i. Ignoring code annotation. En déclarantien dehors de la boucle, ça marche.
Oui, j’ai oublié de corriger cette erreur dans l’un des deux fichiers que j’utilise.
4.3.3.1. Non-mutating: Forall, Exists, ..
Dans cet exercice, je n’ai pas trouvé comment réutiliser le contrat de
predpour définir les autres fonctions. Je voulais écrire quelque chose du genre :/*@ requires \valid_read(a + (0 .. s - 1)); assigns \nothing; ensures \result <==> \forall size_t i; 0 <= i < s ==> pred(a[i]); */ int forall_pred(int* a, size_t s)mais je n’ai pas abouti. J’ai fini par virer
predet considérer les valeurs comme des booléens.En regardant un peu plus loin, j’ai l’impression qu’il faudrait définir un prédicat et le réutiliser pour les autres fonctions, c’est bien ça ? Si oui, je me demande si cet exercice n’aurait pas plutôt sa place plus loin, quitte à garder une version sans
predici.
Il faut que je détaille plus l’exercice. On ne peut effectivement pas utiliser une fonction C dans du code ACSL. Et même si celle-ci indiquait \assigns \nothing on ne pourrait pas, parce que ce n’est qu’un comportement et pas une "vraie" pureté. Il faudrait que j’ajoute un point là dessus d’ailleurs.
Ici, je comptais simplement à ce que le contrat soit quelque part "inliné". Mais c’est effectivement peu clair.
- d’un côté les parties 1, 2, 3 et 4, "Fondamentaux",
- de l’autre 5, 6, 7, "Approfondissement".
A voir. Il faut que je jette un oeil au template tex de ZdS que j’ai un peu modifié pour qu’il corresponde mieux à ce que je fais.
Merci en tous cas 
J’ai corrigé le plupart de ce qui a été pointé par @Aabu. La seule chose qui pour l’instant n’a pas changé, c’est les exercices sur les comportements, je vais en discuter avec des collègues qui bossent avec WP depuis plus longtemps que moi pour voir s’ils n’ont pas des idées qui pourraient faire des exercices plus intéressants sans pour autant être trop complexes. (Je n’ai pas encore changé le PDF sur mon site par contre, ça va venir).
En tout cas, je travaille de nouveau sur la traduction FR, et je vais sûrement avoir des modifications à faire par rapport à la prochaine version de Frama-C qui arrive.
Un peu de suivi.
Frama-C Calcium est sortie et avec ça j’ai eu quelques changements à faire qui sont pour certains notables et pour d’autres plus raisonnables. Dans l’ensemble ça a été relativement rapide. La prochaine version est dispo sous forme LaTeX sur la branche next-version du GitHub du bouquin.
J’ai bien avancé sur la traduction FR. En gros, tout est traduit du début jusqu’au chapitre 5 (cf premier post), c’est dispo sur la branche translate-fr du GitHub.. Il reste le plus gros chapitre du livre à traduire mais j’ai encore un peu de motivation sous le pied pour l’instant. Il restera ensuite un peu de boulot pour porter les quelques changements depuis le moment du diff mais ça reste raisonnable. Après ça, je pourrais commencer à passer tout ça dans la version MD sur ZdS, ce qui va sûrement être moins drôle.
Bref, encore du boulot en perspective mais ça avance.
Encore du suivi. J’ai passé une partie de mon weekend sur le traduction, ce qui fait que :
EDIT : en fait, je vais tenter de faire une pierre deux coups. En transférant le latex vers le markdown pour relire.
Bon. Bah la galerie n’est pas versionnée. Du coup, j’ai flingué la version en ligne.
Bonjour les agrumes !
La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :
Merci d’avance pour vos commentaires.
Il y a beaucoup de nouveau contenu, donc le plus simple pour faire le diff est sûrement de se baser sur la liste présente dans le premier post pour faire des retours sur ce qui est neuf.
Bonjour les agrumes !
La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :
Merci d’avance pour vos commentaires.
(Spellcheck)
Maintenant que le tuto est publié, as-tu encore besoin de la béta? La désactiver permet d’alléger la page de recherche d’aide.
Ah je ne savais pas ça. Je vais la désactiver pour l’instant, même s’il n’est pas exclus que je la réactive bientôt si j’arrive à avancer suffisamment vite.
Bonjour,
La bêta du contenu « Introduction à la preuve de programmes C avec Frama-C et son greffon WP » a été désactivée.
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 cette version :
See: #p222679
Salut,
Je suis content de voir que tu as trouvé des exercices plus intéressants. 
J’ai survolé rapidement, et c’est sympa de voir les progrès des dernières versions !
J’ai une suggestion rapide pour la traduction de « smoke test ». C’est pas évident à traduire, mais je pense que « déverminage » peut être une bonne alternative. Quand ces tests passent, on ne peut pas être sûr à 100% que ça fonctionne, mais on a une certaine assurance qu’il n’y a pas de défaut flagrant sur le produit testé.
J’ai une suggestion rapide pour la traduction de « smoke test ». C’est pas évident à traduire, mais je pense que « déverminage » peut être une bonne alternative. Quand ces tests passent, on ne peut pas être sûr à 100% que ça fonctionne, mais on a une certaine assurance qu’il n’y a pas de défaut flagrant sur le produit testé.
Je me suis penché un peu sur ce qui existe. J’ai l’impression que le terme le plus utilisé même en France est surtout le terme anglais. J’aimais bien aussi l’expression anglaise "sanity-check". Mais sinon, il y a "test préliminaires" qui revient pas mal.
Déverminage si j’ai bien compris c’est plutôt du stress test de démarrage, en anglais il semble que ce soit plutôt associé à "Burn-in" qui est sensiblement différent de "smoke testing" qui semble plutôt associé à la notion de tests préliminaires, je crois que je vais partir là dessus. Surtout qu’on parle de la spécification et pas du code.
Dans l’introduction, ce serait pas « générer à partir de programmes C des exécutables très performants ».
par exemple, nous avons défini que le programme doit trouver la plus petite valeur d’un tableau, mais nous n’avons pas spécifié que s’il y en a plusieurs, il faut prendre la première, parce que cela me semblait trop évident, mais du coup ce n’est pas ce que fait le programme
Plutôt renvoyer l’indice de la plus petite valeur, non ?
Plutôt renvoyer l’indice de la plus petite valeur, non ?
Oui je le sous-entend un peu. J’hésite à le rajouter, ça va alourdir la lecture de l’exemple :thinking: . D’un autre côté c’est un comble d’avoir une imprécision dans un paragraphe qui parle de précision.
EDIT : bon allez, c’est corrigé.
Le reste c’est corrigé aussi, sauf :
« ici : http://frama-c.com/download.html (Source distribution). » problème de mise en forme du lien ?
Parce qu’il y pas de problème c’est voulu.
Merci !
Bonjour les agrumes !
La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :
Merci d’avance pour vos commentaires.
J’ai incorporé vos suggestions Aabu et Karnaj, merci beaucoup à vous deux. J’ai aussi fait une passe de relecture sur le diff complet.
Pour cette version :
-wp-rte presque partout (sauf au tout début)PS: La version TeX est aussi disponible via GitHub sur la branche next-version du bouquin. Si vous voulez faire des retours sur la version anglaise, ne vous privez pas non plus
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