logo Adalog
DataDocké

Méthodes formelles avec Ada et SPARK (3 jours)

Les méthodes formelles, longtemps restées du domaine de la recherche, s'introduisent maintenant dans l'industrie. Ada 2012 a introduit la notion de contrat à l'exécution, alors que SPARK est un langage compatible avec un sous-ensemble d'Ada permettant de prouver formellement des programmes dès la compilation.

Cette formation est une introduction à la programmation formelle, qui permettra aux participants de comprendre son intérêt, et d'évaluer dans quelle mesure elle est applicable à leurs développements, soit en annotant de façon appropriée leurs programmes Ada, soit en franchissant l'étape suivante et en optant pour SPARK.

À la fin de cette formation, les participants sauront comprendre des programmes annotés de spécifications formelles, sauront travailler avec SPARK et GNATprove, par exemple pour vérifier des propriétés importantes, - depuis prouver l'absence d'erreurs à l'exécution jusqu'à prouver complètement l'exactitude fonctionnelle d'algorithmes itératifs simples.

Chacune des trois journées de ce séminaire est constitué d'une session le matin (9:00-13:00), et d'une session l'après-midi (14:00-18:00). Chaque session est partagée entre cours et exercices interactifs. Le cours comporte des démonstrations de programmation en Ada/SPARK.

Les algorithmes sont simples, mais instructifs, pour montrer comment développer du code correct et efficace.

Prérequis

Connaissance élémentaire du langage Ada.

Programme détaillé

  Matin Après-midi
Jour 1
Principes généraux
  • Écriture de spécifications formelles au moyen de contrats; préconditions et postconditions.
  • Annotation du programme: utilisation d'aspects/pragmas Assume, Assert, invariants et variants de boucles.
  • Algorithmes numériques.
  • Techniques d'établissement/découverte des invariants de boucles.
  • Rétro-propagation d'assertions autour des instructions d'affectation.
Jour 2
Perfectionnements
  • Compléments sur les invariants de boucle.
  • Propagation d'assertions autour des instructions if.
  • Algorithmes de recherche avec des tableaux.
  • Réutilisation correcte de sous-programmes.
  • Code fantôme: convaincre GNATprove au moyen de procédures fantômes (lemmes).
Jour 3
Fonctionnalités avancées
  • Algorithmes de manipulation de tableaux: tris.
  • Preuves d'exactitude des lemmes.
  • Techniques avancées de preuve d'exactitude des lemmes.
  • Preuves de l'absence d'erreurs d'exécution.