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

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

@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

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.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

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
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

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