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

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