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 :
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
- [OK] Typos #p222604
- II
- [OK] Smoke tests
- [OK] formulation française #p222516
- [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
- [OK] Smoke tests
- 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
?
- [NEXT]
- 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 !