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.

Bonjour les agrumes !

La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :

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

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

+0 -0

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 » !

Dans un premier temps, les changements ne seront pas disponibles sur ZdS, c’est plus simple pour moi pour le suivi de passer directement par le GitHub du projet, d’autant que je commence systématiquement par rédiger la version anglaise du tutoriel (plus facile pour moi de faire une bonne traduction française que l’inverse).

+1 -0

Bon, ça a bougé moins vite que je ne l’espérais mais ça a bougé quand même. J’ai été pas mal bloqué par des régressions dans le prouveur Alt-Ergo qui sont fixées depuis mai ce qui m’a permis de mettre à jour les tests et de mieux voir où j’en étais sur les exemples.

J’ai repris la rédaction du contenu. Ce qui est déjà fait pour la prochaine version:

  • des éléments de vocabulaires fixés un peu partout,
  • des fixs dans les exercices
  • explications à propos des requires sur la fonction main,
  • refonte des explications sur les variants et ajout des variants généralisés,
  • ajout des clauses terminates (assurer qu’une fonction termine en fonction d’une condition),
  • ajout des clauses decreases (pour les fonctions récursives)
  • explications sur les clusters d’axiomatiques.

En cours et bien avancé:

  • explications sur check, admit et variantes pour les lemmes et les invariants de boucles,
  • expliquer que WP produit plusieurs formules

Prochains travaux:

  • expliquer comment bien spécifier une boucle
  • toucher deux mots des variants check et admit pour les contrats de fonctions
  • attaquer la partie "improving confidence".

Pour le suivi

+1 -0

Update

Ajouté:

  • explications sur check, admit et variantes pour les lemmes et les invariants de boucles,
  • expliquer que WP produit plusieurs formules
  • expliquer comment bien spécifier une boucle

Prochains travaux

  • toucher deux mots des variants check et admit pour les contrats de fonctions
  • attaquer la partie "improving confidence"

Pour le suivi

Note: le PDF sur la branche n’est pas à jour, il faut générer le PDF à la mano

+0 -0
Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

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