Fondamentaux de la vérification algorithmique

📋 Plan du Cours

1. Spécifications d'un algorithme
2. Vérification des pré-conditions
3. Correction d'un algorithme
4. Terminaison
5. Preuve par invariants
6. Preuve par variants
7. Algorithmes simples
8. Algorithmes récursifs
9. Signature d'une fonction
10. Vérification de la signature

📖 1. Spécifications d'un algorithme

🔑 Notions clés & Définitions

• Spécifications : Ensemble des conditions décrivant précisément le cahier des charges d’un programme, notamment les données d’entrée et de sortie attendues. Elles servent de référence pour la conception et la vérification de l’algorithme.
• Données d’entrée et sortie : Les informations que l’algorithme doit recevoir (entrée) et produire (sortie) pour réaliser la tâche demandée, conformément aux spécifications.
• Cahier des charges : Document décrivant les objectifs, contraintes et conditions que doit respecter un programme ou un algorithme, sans préciser son mode de fonctionnement.
• Différence entre spécifications, algorithme et implémentation :
  • Spécifications : décrivent le résultat attendu, le cahier des charges.
  • Algorithme : la démarche ou l’architecture des instructions permettant de répondre aux spécifications.
  • Implémentation : la traduction concrète de l’algorithme dans un langage de programmation.
• Exemple de spécification (recherche dans liste triée) :
  • Données d’entrée : un nombre réel e, une liste L triée dans l’ordre croissant.
    -…