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.