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

Salut tout le monde !

Bon, on peut dire que la fin de la rédaction aura été faite dans la souffrance, la nouvelle version de Frama-C et surtout des prouveurs automatiques, ayant cassé beaucoup de mes exemples et explications. Mais cette fois, il est là, et il est, je l’espère, lisible !

J’ai commencé (vendredi 30 octobre 2015 à 13h53 il y a vachement plus longtemps, sous la forme d’un tutoriel que je pensais faire court) la rédaction d’un tutoriel au doux nom de « Introduction à la preuve de programmes C avec Frama-C et son greffon WP » et j’ai dans l’objectif de proposer en validation un texte aux petits oignons. Je fais donc appel à votre bonté sans limite pour dénicher le moindre pépin, que ce soit à propos du fond ou de la forme. Vous pourrez consulter la bêta à votre guise à l’adresse suivante :

À présent, c’est à vous !

Une version PDF est disponible ici.

(La liste de corrections ci-dessous est là afin de permettre de trouver plus rapidement les points qui avaient posé problème lors des diverses lectures. Le but étant de vérifier que les corrections apportées sont effectivement de bonnes corrections).

Liste des corrections depuis la première bêta :

  • General
    • [OK] Amener les explications à propos de la difficulté de prouver plus tôt.
    • [OK] Vérifier "objectif" -> "obligation"
    • [OK] Taguer les parties théoriques/prise en main pour alléger la courbe d’apprentissage
    • [OK] Fautes d’orthographes des derniers posts de @barockobamo
    • [OK] Faire une passe pour porter les quelques changements Potassium -> Calcium de la version EN
    • [OK] Vérifier screens et comportement des exemples pour Frama-C Calcium.
  • I
    • [OK] model checking pour les questions de spec insuffisante
    • [OK] monitoring formel de code
    • [OK] illustration différence modèle abstrait VS concret
    • [OK] si/alors etc dans les triplets
    • [OK] Edition code source impossible
    • [OK] Option "colorblind"
  • II
    • [OK] Evacuer pré au début de post pour le garder à plus tard
    • [OK] top/bot -> V/F
    • [OK] Dépassement de abs seulement pour le complément à deux,
    • [OK] Plus de détails sur les bullets
    • [OK] Phrase ratée pour l’appel à abs(INT_MIN) prouvant "faux",
    • [OK] Note pour le parsing des annotations pour les versions Neon et avant.
    • [OK] supposition VS pré-condition pour "faux",
    • [OK] code appelant "comment s’en rendre compte ?",
    • [OK] Trouver les bonnes pré-conditions,
    • [OK] incohérence foo/unref dans validité pointeur
    • [OK] A propos du contrôle des RTEs dans incr_a_by_b
    • [OK] Expliquer mieux les propriétés que génèrent les appels successifs <- pas de règle en fait.
    • [OK] 5 Exercices pour les contrats
    • [OK] 5 Exercices pour la partie "bien spécifier"
    • [OK] 6 Exercices pour les comportements
    • [OK] 3 Exercices pour modularité
  • III
    • [OK] Expliquer le concept de règle d’inférence
    • [OK] Revoir syntaxe instruction calcul de WP + règles d’inférence
    • [OK] considération affectation : instruction/expression
    • [OK] Syntaxe du remplacement dans une propriété
    • [OK] Revoir le passage sur la conditionnelle
    • [OK] Ajouter des éléments introductifs plus simples pour l’invariant + préparer terrain du variant
    • [OK] Insister liaison invariant <-> Postcondition
    • [OK] Fusionne les deux premières sous-section
    • [OK] Variante de l’affectation pour le cas des déréférencements de pointeurs
    • [OK] Fin de boucle avant conditionnelle
    • [OK] Ajout d’une section sur les appels de fonction et sur les fonctions récursives
    • [OK] 4 exercices pour les instructions basiques
    • [OK] 4 exercices pour les bases des boucles
    • [OK] 6 exercices pour les boucles
  • IV
    • [OK] Surcharges de prédicats et fonctions
    • [OK] 5 exercices pour les prédicats
    • [OK] 5 exercices pour les fonctions logiques
    • [OK] 5 exercices pour les lemmes
  • V
    • [OK] oubli d’un screen
    • [OK] Code ACSL de tri en secret
    • [OK] Axiomes de somme pour la partie Ghost en secret
    • [OK] Partie finale Ghost légèrement revue
  • VI
    • [OK] Vérification d’absence de runtime errors, approche par contrat minimaux (4 exercices)
    • [OK] Assertion et déclenchement de lemmes (4 exercices)
    • [OK] Lemma-functions et lemma macros (3 exercices - dont un très long)
  • Conclusion
    • [OK] Correction de fautes
    • [OK] Ajout d’une traduction pour la quote du papier de sécurité
    • [OK] Prédicats inductifs
    • [OK] Nouvel exemple d’axiomatique
    • [OK] Contrat de code ghost
    • [OK] 4 exercices pour les prédicats inductifs
    • [OK] 4 exercices pour les définitions axiomatiques
    • [OK] 2 exercices pour le code ghost

Pour Frama-C 21 :

  • General
    • [OK] Vérifier exemples et screens pour Frama-C 21
    • [OK] -wp-rte partout (sauf au tout début)
      • Bon en fait, c’est pénible pour certains exos, mais on maximise quand même
  • I
  • II
    • [OK] Smoke tests
    • [OK] Exercices plus intéressants pour les comportements
      • Fusionner 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
    • [OK] Deux nouveaux exercices
      • Utilise la solution sur les triangle pour remplir une structure
      • Rendu de monnaie
  • III
  • IV
    • [OK] Supprime un paragraphe trop dépendant des versions des prouveurs
    • [OK] Modification de deux exercices pour que Alt-Ergo 2.3.2 en chie plus
  • V
    • [OK] Fix sur des expressions mathématiques (thx @Karnaj)
    • [OK] Mettre à jour la section sur les ghost pour Frama-C 21
    • [OK] Exercices pour les nouvelles notions ghost
    • [OK] La bonne formation des inductifs est vérifiée avec Why3
  • VI
    • [OK] Mets à jour les éléments ghost pour Frama-C 21

Prochaine version :

  • General
    • [TODO] Vérifier exemples et screens pour Frama-C 22
    • [TODO] Passage à la sortie Why3 pour les preuves Coq
  • I
    • [NEXT ?] exemples plus intéressants sur le WP de l’intro
  • II
    • [NEXT] \initialized
    • [NEXT] \object_pointer ?
  • III
    • [NEXT] plus de détails sur les modèles mémoire et leurs hypothèses
  • IV
    • [NEXT] ASCL list abstract type -> Va plutôt servir dans la partie méthodo, mais plus tard
  • V
  • VI
    • [NEXT ?] Regarder idée d’exercice intéressant pour lemma-functions
    • [NEXT ?] Utilisation du prouveur interactif de WP
    • [NEXT ?] Modèles mémoire

Merci !

Édité par Ksass`Peuk

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+5 -0

+1 pour ce tuto. C’est très rare de voir des sites qui présentent les méthodes utilisées pour analyser les programmes et prouver des propriétés dessus. Et c’est super pratique !

J’ai déjà fait de la varification de programmes "à la mano" à l’école, mais jamais utilisé ça avec FramaC (même si j’en avais entendu parler depuis longtemps). Je teste ton tuto dès ce soir !

+1 -0

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

Salut,

Voilà un tuto qui s’annonce des plus intéressant, merci à toi. :)
Je viens de parcourir les deux premiers chapitres et j’ai une ou deux remarques à faire sur le second.

Définition d’un contrat

Nous pouvons alors voir alors que WP échoue à prouver l’impossibilité de débordement arithmétique sur le calcul de -val. Et c’est bien normal parce que -INT_MIN (−231) > INT_MAX (231 − 1).

Je sais que c’est du détail, mais cela n’est faux qu’en représentation en complément à deux qui est, certes, la représentation utilisée sur l’écrasante majorité des machines, mais n’est pas la seule.

Nous l’ajoutons donc comme pré-condition (à noter : il faut également inclure le header où INT_MIN est défini) :

De mon côté, si j’emploie INT_MIN, le programme frama-c-gui rencontre une erreur parce que le symbole INT_MIN n’existe pas. Ceci me paraît cohérent puisque le préprocesseur est chargé d’éliminer les commentaires du code source et qu’il ne remplacera donc pas INT_MIN par sa valeur.

Dans le premier cas, nous apprenons nécessairement "faux", pas dans le deuxième cas.

Je pense qu’il manque un « pas » avant « nécessairement ».

De l’importance d’une bonne spécification

Séparation des zones de la mémoire

Et cette fois, la preuve est effectuée :

Je suppose que le texte se concentre sur la preuve par le module WP, mais il manque encore la vérification du non débordement d’entier.

#JeSuisArius

+1 -0
Auteur du sujet

Merci pour les retours et l’intérêt ;) .

Nous pouvons alors voir alors que WP échoue à prouver l’impossibilité de débordement arithmétique sur le calcul de -val. Et c’est bien normal parce que -INT_MIN (−231) > INT_MAX (231 − 1).

Je sais que c’est du détail, mais cela n’est faux qu’en représentation en complément à deux qui est, certes, la représentation utilisée sur l’écrasante majorité des machines, mais n’est pas la seule.

Taurre

C’est noté. Je vais changer ça. En fait, Frama-C détecte la configuration de la machine.

Nous l’ajoutons donc comme pré-condition (à noter : il faut également inclure le header où INT_MIN est défini) :

De mon côté, si j’emploie INT_MIN, le programme frama-c-gui rencontre une erreur parce que le symbole INT_MIN n’existe pas. Ceci me paraît cohérent puisque le préprocesseur est chargé d’éliminer les commentaires du code source et qu’il ne remplacera donc pas INT_MIN par sa valeur.

Taurre

Quelle version de Frama-C (Help -> About), quel OS et quel compilateur ?

Normalement le preprocessing des annotations (au moins pour les defines simples) est activé par défaut depuis au moins 2 versions (EDIT : c’est automatique au moins depuis Frama-C Sodium (11), la version actuelle étant Silicium (14)), à partir du moment où le compilateur détecté est un GCC like.

Tu peux essayer en ajoutant les options "-annot -pp-annot" lors du lancement stp ? Je ne peux plus même plus build les versions qui précèdent, j’ai des paquets de bibliothèques trop récents :lol: .

Dans le premier cas, nous apprenons nécessairement "faux", pas dans le deuxième cas.

Je pense qu’il manque un « pas » avant « nécessairement ».

Taurre

"Cette phrase est complètement pourrie, je vais la refaire." (Knarf, grand philosophe de notre temps)

Séparation des zones de la mémoire

Et cette fois, la preuve est effectuée :

Je suppose que le texte se concentre sur la preuve par le module WP, mais il manque encore la vérification du non débordement d’entier.

Taurre

Le but était surtout d’illustrer la notion de séparation. Je vais mettre un bout de texte pour évacuer le reste de la preuve.

Édité par Ksass`Peuk

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+0 -0

Quelle version de Frama-C (Help -> About), quel OS et quel compilateur ?

Ksass`Peuk

Effectivement, mon message manquait de détails. :p
Donc sous Debian Jessie avec Frama-C Neon-20140301 (dont la compilation date du 29 avril 2014 apparemment) avec GCC 4.9.2.

Normalement le preprocessing des annotations (au moins pour les defines simples) est activé par défaut depuis au moins 2 versions (EDIT : c’est automatique au moins depuis Frama-C Sodium (11), la version actuelle étant Silicium (14)), à partir du moment où le compilateur détecté est un GCC like.

Tu peux essayer en ajoutant les options "-annot -pp-annot" lors du lancement stp ? Je ne peux plus même plus build les versions qui précèdent, j’ai des paquets de bibliothèques trop récents :lol: .

Ksass`Peuk

Yep, cela fonctionne avec les options -annot -pp-annot à condition qu’elles soient renseignées avant l’option -rte (ce qui est assez bizarre puisque le problème ne se pose pas avec -wp seule, mais bref…). :)

Édité par Taurre

#JeSuisArius

+1 -0
Auteur du sujet

Donc sous Debian Jessie avec Frama-C Neon-20140301 (dont la compilation date du 29 avril 2014 apparemment) avec GCC 4.9.2.

Taurre

Ok, du coup, vu qu’on a l’info je vais mettre un aparté à cet endroit vu que Jessie est quand même pas mal utilisée. Après, tu vas sûrement avoir d’autres surprises au fil du tutoriel. En particulier avec le contenu des obligations de preuve et les capacités des prouveurs qui ont énormément évolué depuis.

À noter : même sous Jessie, en passant par Opam, il y a moyen d’avoir des versions assez récentes.

Yep, cela fonctionne avec les options -annot -pp-annot à condition qu’elles soient renseignées avant l’option -rte (ce qui est assez bizarre puisque le problème ne se pose pas avec -wp seule, mais bref…). :)

Taurre

Oui, la ligne de commande a aussi pas mal évolué depuis Neon, notamment en ce qui concerne certaines options qui créent un contexte dans la ligne pour pouvoir faire certaines choses juste en ligne de commande. Je n’en parle pas vu qu’on la manipule très peu dans le tutoriel.

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+0 -0

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

Plop,

Je viens lire le chapitre trois et… c’est tout de suite un peu plus corsé à lire pour moi. ^^"

Tout d’abord, je me demandais : est-ce qu’il est possible d’obtenir un peu plus d’information lorsqu’une preuve n’est pas possible ? Il est montré comment obtenir un peu plus de détails via l’onglet « WP Goals », mais j’avoue que cela ne m’éclaire personnellement pas trop. Il y a moyen que le programme soit plus verbeux ?

Sinon, j’aurais juste deux petites questions suite à me lecture :

  • l’instruction loop variant [exp]; est-elle vraiment nécessaire ? Je veux dire, en notant un invariant comme loop invariant 0 <= i <= [max];, il n’est pas possible de prouver que la boucle se termine ?
  • pourquoi le code ci-dessous ne peut-il pas être prouvé (je suppose que cela est lié à la modification de la variable a, mais je ne vois pas) ? :-°
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
/*@
    requires INT_MAX - 10 >= a;
    ensures \result == \old(a) + 10;
*/
int
plus_dix(int a)
{
    int i;

    /*@
        loop invariant 0 <= i <= 10;
        loop assigns i, a;
        loop variant 10 - i;
    */
    for (i = 0; i < 10; ++i)
        ++a;

    return a;
}

Enfin, j’ai juste une ou deux remarques à faire.

Affectation, séquence et conditionnelle

Règle d’affectation

L’affectation est l’instruction la plus basique du langage C.

C’est à nouveau du détail, mais l’affectation n’est pas une instruction, mais une expression (et ce n’est pas la plus simple parmis ces dernières si tant est qu’il y en ait une ^^ ).

Sinon, dans la formule qui suit, il y a une suite « ;, », est-ce normal ou bien est-ce une faute de frappe ? Aussi, c’est peut-être moi qui ne suit pas en parcourant les différentes formules, mais cela ne devrait pas être « PréCondition » à droite de l’égalité et non « PostCondition » ?

De manière générale, je ne sais pas si c’est moi, mais l’utilisation de fraction me perturbe pas mal parce que je ne comprend pas bien sa signification dans ce cas ci (je suppose qu’il n’est pas question de fraction ? ).

#JeSuisArius

+1 -0
Auteur du sujet

Je viens lire le chapitre trois et… c’est tout de suite un peu plus corsé à lire pour moi. ^^"

Taurre

S’il y a des trucs qui ne sont pas clairs, hésite pas à lister, je verrai ce que je peux améliorer.

Tout d’abord, je me demandais : est-ce qu’il est possible d’obtenir un peu plus d’information lorsqu’une preuve n’est pas possible ? Il est montré comment obtenir un peu plus de détails via l’onglet « WP Goals », mais j’avoue que cela ne m’éclaire personnellement pas trop. Il y a moyen que le programme soit plus verbeux ?

Taurre

L’onglet WP Goals, c’est plus quand on commence à bien maîtriser l’outil qu’il devient utile. Je ne m’en sers ici que pour illustrer certains points vraiment simples à comprendre. Dans certains cas, cela permet de remarquer qu’il est impossible de conclure parce qu’il manque vraiment une info.

Pour la verbosité, malheureusement non. C’est la faiblesse de la preuve automatique. Les outils peuvent prouver beaucoup de choses par eux-mêmes mais en contre-partie ils ne remontent que peu d’information. Ce sont des SMT solvers, une généralisation des solveur SAT. Et un solveur SAT, ça répond rarement plus que SAT, UNSAT ou unknown. Il y a des travaux pour générer des contre-exemples à partir des preuves en combinaison avec de la génération automatique de tests mais c’est un autre greffon de Frama-C et je ne suis pas sûr qu’il soit accessible publiquement (les papiers de recherche de Guillaume Petiot sont par contre disponible et expliquent le rôle du greffon).

Pour mieux comprendre le processus de preuve et ses échecs, il faut passer par de la preuve interactive, avec Coq par exemple. Cependant, il faut être assez habitué à Coq, sinon, on a vite fait d’être perdu à cause de l’implémentation de la sémantique du C qui peut rendre les obligations de preuve difficiles à lire.

  • l’instruction loop variant [exp]; est-elle vraiment nécessaire ? Je veux dire, en notant un invariant comme loop invariant 0 <= i <= [max];, il n’est pas possible de prouver que la boucle se termine ?
Taurre

Oui le variant est nécessaire. Avec un invariant comme loop invariant 0 <= i <= [max]; on ne peut pas conclure. Par exemple, la boucle suivante respecte l’invariant en question mais ne termine pas :

1
2
3
/*@ loop invariant 0 <= i <= 10; */
for(int i = 0; i < 1; ++i)
  --i;
  • pourquoi le code ci-dessous ne peut-il pas être prouvé ? :-°
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
/*@
    requires INT_MAX - 10 >= a;
    ensures \result == \old(a) + 10;
*/
int
plus_dix(int a)
{
    int i;

    /*@
        loop invariant 0 <= i <= 10;
        loop assigns i, a;
        loop variant 10 - i;
    */
    for (i = 0; i < 10; ++i)
        ++a;

    return a;
}
Taurre

Parce que l’invariant n’établit pas de relation entre a et i. L’invariant doit préciser cela. Pour rependre la construction des plus faibles pré-condition : on cherche à prouver \result == \old(a) + 10, on sait : i == 10 grâce à l’invariant et la condition, donc on ne sait pas comment faire. Il faut ajouter : loop invariant a == \at(a,Pre)+i; (par exemple).

L’affectation est l’instruction la plus basique du langage C.

C’est à nouveau du détail, mais l’affectation n’est pas une instruction, mais une expression (et ce n’est pas la plus simple parmis ces dernières si tant est qu’il y en ait une ^^ ).

Taurre

Ah oui, effectivement d’après la norme c’est une expression. A vrai dire j’ai repris les dénominations choisies par la bibliothèque CIL qui est utilisée pour représenter l’AST du programme d’entrée. Après, l’affectation reste considérée comme une instruction dans la majorité des langages et introduire encore du vocabulaire serait peut être raide. Je vais voir ce que je peux faire pour pas trop surcharger.

Sinon, dans la formule qui suit, il y a une suite « ;, », est-ce normal ou bien est-ce une faute de frappe ?

Taurre

C’était volontaire, mais en fait en relisant, je trouve ça laid. Je vais chercher un truc mieux (y compris pour les formules suivantes).

Aussi, c’est peut-être moi qui ne suit pas en parcourant les différentes formules, mais cela ne devrait pas être « PréCondition » à droite de l’égalité et non « PostCondition » ?

Taurre

Non, c’est bien PostCondition pour le coup. La raison est assez simple : tu cherches à trouver la plus faible pré-condition d’une certaine post-condition : donc tu n’as pas de pré-condition manipulable à cet endroit, c’est ce que tu calcules. Et ce que cela exprime c’est : la plus faible pré-condition de l’action "x = E" pour une PostCondition voulue, est cette même PostCondition où les occurrences de "x" sont remplacées par "E".

De manière générale, je ne sais pas si c’est moi, mais l’utilisation de fraction me perturbe pas mal parce que je ne comprend pas bien sa signification dans ce cas ci (je suppose qu’il n’est pas question de fraction ? ).

Taurre

Non effectivement, c’est ce que l’on appelle une règle d’inférence. Je vais mettre une introduction là-dessus car c’est vrai que ce n’est pas très naturel comme notation quand on ne connaît pas le domaine.

Ce que cela exprime grossièrement c’est : ce qui est en bas est vrai, si les différentes prémisses au dessus sont vraies. L’idée étant que lorsque l’on applique récursivement le processus, cela produit ce qu’on appelle l’arbre de preuve.

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+0 -0

S’il y a des trucs qui ne sont pas clairs, hésite pas à lister, je verrai ce que je peux améliorer.

Ksass`Peuk

Ben, je pense que je me suis un peu perdu dans les explications d’invariant et de variant. Je pense qu’il pourrait être bon de donner une définition de l’invariant sans s’attarder sur les pré et post-conditions dans un premier temps : un invariant est une propriété qui est vraie avant et après chaque répétition (et donc au début et à la fin de la boucle). C’est ce que dit ton explication, mais il me semble que c’est moins limpide (peut-être parce qu’il y a beaucoup de formalisation à ce niveau).

De même pour le variant de boucle, je pense qu’il serait peut-être judicieux d’en parler plus tôt, histoire d’insister sur le fait que l’invariant ne prouve pas l’arrivée à la fin de la boucle, mais uniquement qu’une certaine propriété sera vrai d’une répétition à l’autre (mais bon, ça c’est plus pour moi :p ). Aussi, peut-être plutôt le décrire comme une expression permettant de calculer, à chaque tour, le nombre d’itérations qui reste à réaliser (et après seulement préciser que, de ce fait, il peut permettre de connaître le nombre maximal d’itérations).

Pour la verbosité, malheureusement non. C’est la faiblesse de la preuve automatique. Les outils peuvent prouver beaucoup de choses par eux-mêmes mais en contre-partie ils ne remontent que peu d’information. Ce sont des SMT solvers, une généralisation des solveur SAT. Et un solveur SAT, ça répond rarement plus que SAT, UNSAT ou unknown. Il y a des travaux pour générer des contre-exemples à partir des preuves en combinaison avec de la génération automatique de tests mais c’est un autre greffon de Frama-C et je ne suis pas sûr qu’il soit accessible publiquement (les papiers de recherche de Guillaume Petiot sont par contre disponible et expliquent le rôle du greffon).

Pour mieux comprendre le processus de preuve et ses échecs, il faut passer par de la preuve interactive, avec Coq par exemple. Cependant, il faut être assez habitué à Coq, sinon, on a vite fait d’être perdu à cause de l’implémentation de la sémantique du C qui peut rendre les obligations de preuve difficiles à lire.

Ksass`Peuk

Ok, c’est dommage, mais on fera sans.

Parce que l’invariant n’établit pas de relation entre a et i. L’invariant doit préciser cela. Pour rependre la construction des plus faibles pré-condition : on cherche à prouver \result == \old(a) + 10, on sait : i == 10 grâce à l’invariant et la condition, donc on ne sait pas comment faire. Il faut ajouter : loop invariant a == \at(a,Pre)+i; (par exemple).

Ksass`Peuk

Ok, je comprends mieux, merci. :)

Ah oui, effectivement d’après la norme c’est une expression. A vrai dire j’ai repris les dénominations choisies par la bibliothèque CIL qui est utilisée pour représenter l’AST du programme d’entrée. Après, l’affectation reste considérée comme une instruction dans la majorité des langages et introduire encore du vocabulaire serait peut être raide. Je vais voir ce que je peux faire pour pas trop surcharger.

Ksass`Peuk

Effectivement, le C (et, du coup, ceux qui s’en sont inspirés) est plutôt une exception de ce côté, mais cela fait pas mal de différence puisque cela permet par exemple d’écrire if ((ptr = malloc(5)) == NULL).

Non, c’est bien PostCondition pour le coup. La raison est assez simple : tu cherches à trouver la plus faible pré-condition d’une certaine post-condition : donc tu n’as pas de pré-condition manipulable à cet endroit, c’est ce que tu calcules. Et ce que cela exprime c’est : la plus faible pré-condition de l’action "x = E" pour une PostCondition voulue, est cette même PostCondition où les occurrences de "x" sont remplacées par "E".

Ksass`Peuk

Ah ! Ok, je n’avais pas compris cela à la lecture (faut dire que j’ai un peu de mal avec la formalisation en général :-° ).

Ce que cela exprime grossièrement c’est : ce qui est en bas est vrai, si les différentes prémisses au dessus sont vraies. L’idée étant que lorsque l’on applique récursivement le processus, cela produit ce qu’on appelle l’arbre de preuve.

Ksass`Peuk

Ok, voilà qui est plus clair, merci. ^^

#JeSuisArius

+0 -0

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

Bonjour, Dans le chapitre sur les Pointeurs, Validité de pointeurs, cette phrase : "Le déréférencement de p est valide, pourtant la pré-condition de foo ne sera pas validée…" Dans l’exemple la fonction s’appelle unref.

– barock

+1 -0
Auteur du sujet

Bonjour les agrumes !

La bêta a été mise à jour avec les commentaires de @Taurre et @barockobamo .

N’hésitez pas à aller rejeter un oeil aux points "corrigés" pour assurer que ce sont bien des corrections et pas des "corrections".

Merci d’avance pour vos commentaires.

Édité par Ksass`Peuk

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+0 -0

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

Bonjour Bayonne ! On s’en paye une tranche ? :

  • chapitre Comportements :
  • … bien tout le domaine des entées.
  • … Nous pouvons voir que la combinaison des appels se traduit du côté de la spécification comme une combinaison des spécifications des fonctions appelées sur les variables concernées.(OK) Ceci est valable à la fois pour les pré et les post-conditions. (OK) Plus nous combinons les appels, plus les entrées se restreignent et plus les sorties se multiplient. (Pas tout a fait clair pour mes 2 neurones o_O)
  • chapitre Instructions basiques et structures de contrôle :
  • Triplet de Hoare : nous calcule la pré-condition minimale assurant Q après C.
  • Affectation : Où P[x←E] signifie "P où x est remplacé par E". Au dessus il est question de PostCondition[x←E]
  • Règle de la Conditionnelle : A noter que suivant cette définition, si le else ne fait rien, alors nous devons avoir : Pre∧¬B⇒Post (Une petite explication supplémentaire serait la bienvenue pour les Newbies, ou alors une 2ème règle pour le if sans else, ce serait plus clair :-° )

La suite au prochaine épisode,

barock

+1 -0
Auteur du sujet

Bonjour Bayonne ! On s’en paye une tranche ?

** Clin d’oeil appuyé **

Plus nous combinons les appels, plus les entrées se restreignent et plus les sorties se multiplient. (Pas tout a fait clair pour mes 2 neurones o_O)

barockobamo

Ouais j’aimais pas cette phrase non plus la dernière fois que j’ai relu, je vais écrire quelque chose de moins pire.

EDIT : en fait c’est plutôt simple : il suffit de virer cette remarque. Il n’y a pas de règle en fait.

  • Affectation : Où P[x←E] signifie "P où x est remplacé par E". Au dessus il est question de PostCondition[x←E]
barockobamo

Ouais, je vais revoir l’explication. C’est de la notation que je veux parler avec cette phrase. Mais du coup avec une seule phrase, soit ça n’explique pas la notation, soit ça n’explique pas la propriété.

  • Règle de la Conditionnelle : A noter que suivant cette définition, si le else ne fait rien, alors nous devons avoir : Pre∧¬B⇒Post (Une petite explication supplémentaire serait la bienvenue pour les Newbies, ou alors une 2ème règle pour le if sans else, ce serait plus clair :-° )
barockobamo

Oui, mais c’est plus une conséquence de la règle qu’une autre règle, donc je vais revoir un peu l’explication.

EDIT : En fait, je vais revoir beaucoup l’explication, c’est l’ensemble de la section qui ne me convient pas.

Édité par Ksass`Peuk

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+0 -0

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

Hello Donald c’est Ivana,

Les boucles - Exemples | Exemple avec un tableau read-only

//pour tout "off" de type "size_t", tel que SI "off" est compris entre 0 et "length" // ALORS la case "off" de "a" vaut "element" \forall size_t off ; 0 <= off < length ==> a[off] != element; Ce n’est pas plutôt "ne vaut pas" ? / behavior notin

ACSL - Propriétés | Fonctions logiques

Les fonctions logiques nous permettent de décrire des fonctions qui ne seront utilisables que dans les spécifications. Cela nous permet d’un part ... une

ACSL - Propriétés | Exemple : propriété fonction affine

  • requires limit_int_min_ax_b(_,_) ... limit_int_max_ax_b(_,_); *Ce qui est définie plus haut c’est * logic integer limit_min_ax_b et logic integer limit_max_ax_b
  • Toutes les techniques expliquées dans cette partie sontsure ...sûres/sures

C’est tout pour aujourd’hui, c’est du beau boulot !

ivanotrumpa

+1 -0

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

Final Countdown today,

ACSL - Définitions logiques et code | Définition de fonction ou prédicats récursifs

  • Et d’énoncer une assertion pour spécifier ce qui n’a pas changé entre le début du bloc de la boucle et la fin : ... //@ assert same_elems{L,Here}(array,0,i) Une petite précision supplémentaire sur les labels quelque part serait pas mal, ici on comprends bien Here, mais où est L ? / Désolé pour mon cerveau lent, je débute, mais peut-être que d’autres seront dans le même cas …

ACSL - Définitions logiques et code | Consistance

  • Notamment parce que par exemples ... / exemple

ACSL - Définitions logiques et code | Exemple : le tri

  • Nous laissons au lecteur le loisir de spécifier et prouver les fonctions de recherche du minimum et d’échange de valeur. comme c’est un tuto sur un truc compliqué et que je suis un lecteur feignant j’aurai préféré que l’auteur continue de gentille-ment nous le montrer …

ACSL - Définitions logiques et code | Code Fantôme | Expliciter un état logique

  • ce n’est pas très complexe, nous laissons au lecteur le loisir de poser les axiomes nécessaires idem (partout)

ACSL - Définitions logiques et code | Expliciter un état logique

  • ... Le lecteur pourra se pencher sur cet exercice à l’envie. idem, d’accord mais comment ? soit on nous le montre ne serait-ce qu’un peu, soit on n’aborde pas forcément le sujet

Pour conclure

Un grand merci, c’est de loin la meilleure introduction que j’ai lu depuis 3 mois, car axée prise en main de l’outil, relativement exhaustive et plus facile à lire qu’un article. Il pourrait être utile de tagger les parties théoriques les plus abruptes (Preuves, Règles et Calcul de WP dans le chapitre Instructions basiques et structures de contrôle ) par un message "peut être réservé à une deuxième lecture", on comprends mieux le travail de spécifications sur le code que la partie théorique (en tout cas dans un premier temps). J’espère que mes remarques ont été utiles et qu’elles ne t’ont pas découragées pas leur manque de profondeur, mais c’est toujours pareil, quand on ne sait pas, on découvre tout !

Chapeau l’artiste !

+2 -0
Auteur du sujet

Merci pour tous tes retours. Les fautes d’orthographes/expression sont déjà corrigées dans la version offline. Je vais transformer les parties en mode lecteur feignant. Le but était à la base que le lecteur s’exerce un peu. Du coup, je vais mettre ça en balise secret et indiquer un point exo juste avant.

Pour la distinction théorique prise en main, je vais me pencher dessus plus longuement. Notamment parce qu’il va du coup falloir que je veille à ne pas fournir deux fois les explications (en refondant) ou pire, à me baser sur une explication qui n’existe plus hors de la partie théorique quand je parle du technique.

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+0 -0
Auteur du sujet

Bonjour les agrumes !

La bêta a été mise à jour avec presque tout les points précédemment cités. La prochaine version devrait intégrer le dernier point manquant : une séparation plus nette entre formel et technique. Cependant je ne donne pas encore de deadline pour ce point.

EDIT : certaines fautes dans la conclusion sont déjà corrigées dans la version brouillon. Une traduction a également ajoutée pour le passage en anglais dans cette même conclusion.

Merci d’avance pour vos commentaires.

Édité par Ksass`Peuk

[Tutoriel, Preuve de programmes C avec Frama-C WP]

+1 -0
Ce sujet est verrouillé.