Vérification et complexité
Cette UE compte 30h d'enseignement pour 3 ECTS.
Nous utiliserons essentiellement les documents
de Yannick Le Bras
que je mets régulièrement à jour et ceux de
de Rustan Leino.
Je remercie chaleureusement ces collègues pour leur générosité !
Chaque séance comporte une partie cours et une partie TD.
Tous les documents nécessaires à la réussite de cette UE sont disponibles à partir de cette page.
Plan
- An impossible program,
indécidabilité du problème de l'arrêt
- Terminaison (Yannick Le Bras, exercices inclus)
- Correction (Yannick Le Bras, exercices inclus)
- Notation asymptotique : O() et Θ()
(Sylvie Hamel),
exercices
- Complexité algorithmique (Yannick Le Bras, exercices inclus),
exercices complémentaires
(Etienne Payet)
Evaluation
Contrôle continu : une interrogation et un contrôle terminal écrit, tous deux sans document ni moyen électronique, 50% + 50%
Deuxième session : examen écrit sans document ni moyen électronique, tout est au programme, 100%
Annales
Ressources
La programmation par contrat
Documents (Rustan Leino)
Exercices
- Installer VS Code et Dafny
- Refaire les exemples et les exos des vidéos de Rustan Leino
- Suivre le guide Dafny
- Etudier les tutoriaux consacrés à la terminaison,
aux ensembles, aux séquences, aux collections et aux lemmes
- Exercices en Dafny
- Exercices de calcul de plus faibles préconditions
Bibliographie
- Logic in Computer Science : Modeling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
- Program Proofs, K. Rustan M. Leino, MIT Press, 2023.
