Introduction à Dafny

La programmation par contrat

• Dafny chez Microsoft, Dafny chez GitHub
• Résumé de la syntaxe Dafny
• Intro vidéo :
  1. Cours 0
  2. Cours 1
  3. Cours 2, binary_search
  4. Cours 3
• La programmation par contrat est basée sur le calcul des plus faibles préconditions d'Edsger Dijkstra (diapos ci-dessous de Srinivas Pinisetty et Rajeev Goré)
  1. Introduction
  2. Variations sur le si-alors-sinon
  3. La boucle tant-que
  4. La boucle tant-que avec invariant et variant

Exercices

1. Installer VS Code et Dafny
2. Refaire les exemples et les exos des vidéos de Rustan Leino
3. Suivre le guide Dafny
4. Etudier les tutoriaux consacrés à la terminaison, aux ensembles, aux séquences, aux collections et aux lemmes
5. Exercices en Dafny
6. Exercices de calcul de plus faibles préconditions

Bibliographie

• Program Proofs, K. Rustan M. Leino, MIT Press, 2023.