Introduction à la preuve de programmes C avec Frama-C et son greffon WP

Introduction à la spécification et la preuve de programmes C, par l'usage de Frama-C, du langage ACSL et son greffon WP. Quelques rudiments théoriques sont donnés.

a marqué ce sujet comme résolu.
Auteur du sujet

Reprise du dernier message de la page précédente

@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 ?

Ksass`Peuk

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.

+0 -0

Cette réponse a aidé l’auteur du sujet

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.

  • 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.
  • Les behaviors permettent de s’assurer d’avoir pris en compte toutes les combinaisons d’entrées, tout en gardant une formulation plutôt naturelle avec la clause qui va bien (y compris avec la clause de sûreté !).
  • Garder la propriété de sûreté indépendante ouvre un choix de spécification dans les behaviors (soit on laisse l’état suivant fixé formellement, soit on arrête un choix donné).
  • L’implémentation n’est pas forcément un calque des spec (par exemple, on pourrait faire le if sur le watchdog au plus haut niveau, et pas comme j’ai fait) et pourrait dépendre de détails concrets de la machine sans changer la spec (par exemple s’il y a une séquence d’actions à suivre pour s’éteindre).

Bref, c’était improvisé, mais assez formateur finalement. Je suis parti un peu loin. :D

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…

+0 -0
Auteur du sujet

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…

Aabu

(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.

Cette réponse a aidé l’auteur du sujet

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 :

  • d’un côté les parties 1, 2, 3 et 4, "Fondamentaux",
  • de l’autre 5, 6, 7, "Approfondissement".

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.

Édité par Aabu

+0 -0
Auteur du sujet

Il me semblait avoir répondu à ce message mais en fait pas du tout. Désolé @Aabu :honte: .

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éclarant i en 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 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.

Aabu

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".
Aabu

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 :)

Auteur du sujet

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.

Édité par Ksass`Peuk

Auteur du sujet

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.

Auteur du sujet

Encore du suivi. J’ai passé une partie de mon weekend sur le traduction, ce qui fait que :

  • la version FR est presque prête, il ne reste qu’à faire une relecture profonde puis je passerai le tout en markdown ici,
  • la version EN a un peu évolué (quelques scripts mis à jour pour Coq, quelques explications changées),
  • la version FR a suivi le mouvement.

EDIT : en fait, je vais tenter de faire une pierre deux coups. En transférant le latex vers le markdown pour relire.

Édité par Ksass`Peuk

Auteur du sujet

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.

Édité par Ksass`Peuk

Auteur du sujet

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

Édité par Ksass`Peuk

Cette réponse a aidé l’auteur du sujet

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é.

+0 -0
Auteur du sujet

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é.

Aabu

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.

Cette réponse a aidé l’auteur du sujet

Dans l’introduction, ce serait pas « générer à partir de programmes C des exécutables très performants ».

La preuve de programmes et notre outil pour ce tutoriel : Frama-C

  • « Le test de programme peut être utilisé ».
  • « Et il s’avère généralement que, bien qu’assez vraie, cette phrase soit est assez mal comprise.
  • au premier point des trois catégories de code, il manque l’espace avant le point-virgule final, « pendant une recherche de minimum) ; »

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 ?

  • « à la spécification de notre langage, ;
  • « on parle de « satisfiabilité »
  • dans le bloc attention de la sous-section Installation, des points-virgules à la place des virgules en fin d’éléments de liste.
  • « il faut également que quelques paquets de votre distribution soi*ent présents »
  • « ici : http://frama-c.com/download.html (Source distribution). » problème de mise en forme du lien ?

Assez des salamis, je passe au jambon — Je fais un carnage si ce car nage car je nage, moi, Karnaj ! — Le comble pour un professeur de mathématique ? Mourir dans l’exercice de ses fonctions.

+0 -0
Auteur du sujet

Plutôt renvoyer l’indice de la plus petite valeur, non ?

Karnaj

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 !

Édité par Ksass`Peuk

Auteur du sujet

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 :

  • General
    • Vérifier exemples et screens pour Frama-C 21
    • Spellcheck du diff
    • -wp-rte presque partout (sauf au tout début)
  • I
  • II
    • Smoke tests
    • Exercices plus intéressants pour les comportements
      • Fusionne les exercices 1 à 4 en un seul
      • Ajoute un exercice avec deux fonctions très simples
      • Ajoute un exercice avec deux fonctions à peine plus complexes à propos des triangles
    • Deux nouveaux exercices
      • Utilise la solution sur les triangle pour remplir une structure
      • Rendu de monnaie
  • IV
    • Supprime un paragraphe trop dépendant des versions des prouveurs
    • Modification de deux exercices pour que Alt-Ergo 2.3.2 en chie plus
  • V
    • Fix sur des expressions mathématiques (thx @Karnaj)
    • Mise à jour de la section sur les ghost pour Frama-C 21
    • Exercices pour les nouvelles notions ghost
    • La bonne formation des inductifs est vérifiée avec Why3
  • VI
    • Met à jour les éléments ghost pour Frama-C 21

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 :)

Édité par Ksass`Peuk

Ce sujet est verrouillé.