Hoja de repaso: Introduction à l'Algorithmique et Vérification

1. 📌 L'essentiel

• La programmation impérative repose sur l'utilisation de variables, types, instructions et structures de contrôle.
• La logique de Hoare permet de prouver la correction des programmes via des triplets pré et invariants.
• La preuve de terminaison s'appuie sur des quantités de contrôle, suites monotones et bornées.
• Les invariants sont essentiels pour assurer la correction partielle des boucles.
• La norme C23 définit les types, opérateurs, conversions et gestion des erreurs.
• La compilation comprend plusieurs étapes : prétraitement, compilation, assemblage, lien.
• Exemples clés : échange de valeurs, calcul de factorielle, suite de Fibonacci, suite de Collatz.
• La correction d’un programme consiste à prouver qu’il répond à la spécification si il se termine.
• La construction d’algorithmes corrects s’appuie sur la hiérarchie des invariants et la preuve de terminaison.
• La maîtrise des types en C permet d’éviter erreurs et de gérer efficacement la mémoire.

2. 🧩 Structures & Composants clés

• Variables / Types — stockent des données, scalaires (arithmétiques, caractères, énumérés, flottants, pointeurs).
• Instructions — affectation, lecture, écriture, séquentielle, alternative, boucle.
• Invariants — assertions stables dans une boucle, clés pour la preuve de correction.
• Assertions / Triplets Hoare — (P, A, P′) : précondition, instruction, post-condition.
• Quantités de contrôle — variables ou expressions qui garantissent la terminaison.
• Fichiers C — sources (.h, .c), objets (.o), étapes de compilation.

3. 🔬 Fonctions, Mécanismes & Relations

• Logique de Hoare :
  • Règles pour composition séquentielle, alternative, boucle.
  • Invariants pour prouver la correction partielle.
• Preuves :
  • Correction : si le programme se termine, il satisfait la spécification.
  • Terminaison : suite monotone, bornée, quantités de contrôle.
• Exemples :
  • Échange : prouver la correction, boucle simple.
  • Factorielle : invariant Q : 0 ≤ k ≤ n ∧ f = k! ; boucle jusqu’à k = n.
  • Fibonacci : somme croissante/décroissante.
  • Collatz : preuve de terminaison par invariants et suites monotones.

4. Tableau comparatif : Types en C

5. 🗂️ Diagramme hiérarchique

Algorithme
 ├─ Variables et types
 ├─ Instructions élémentaires
 ├─ Construction correcte
 │   ├─ Invariants
 │   └─ Terminaison
 ├─ Logique de Hoare
 └─ Exemples concrets

6. ⚠️ Pièges & Confusions fréquentes

• Confondre invariants de boucle et assertions temporaires.
• Oublier de prouver la terminaison, seul le correctif partiel est assuré.
• Mauvaise utilisation des règles de Hoare, notamment dans la composition.
• Confusion entre types signés et non signés en C.
• Ignorer la gestion des erreurs lors des conversions ou accès mémoire.
• Négliger la mise en place d’un invariant lors de la conception.
• Confondre la correction partielle et la correction totale.
• Omettre la preuve de terminaison dans l’analyse d’un algorithme.

7. ✅ Checklist Examen Final

• Définir un algorithme et ses instructions principales.
• Expliquer la logique de Hoare et ses triplets.
• Préciser le rôle des invariants dans la preuve.
• Savoir prouver la correction partielle d’un programme simple.
• Savoir prouver la terminaison via quantités de contrôle.
• Connaître les types fondamentaux en C et leurs limites.
• Décrire le processus de compilation d’un programme C.
• Illustrer avec un exemple : échange, factorielle, Fibonacci, Collatz.
• Identifier les erreurs fréquentes en programmation et vérification.
• Maîtriser la hiérarchie des invariants et leur rôle dans la correction.
• Comprendre la différence entre correction partielle et totale.
• Savoir utiliser assertions et invariants pour la vérification.
• Être capable d’écrire un invariant pour une boucle donnée.
• Connaître les étapes pour prouver la terminaison d’un algorithme.
• Être à l’aise avec la syntaxe et la sémantique des types en C.
• Savoir analyser un programme pour détecter erreurs potentielles.
• Connaître la structure générale d’un fichier source et d’un fichier objet.

Ce résumé synthétique t’aidera à cibler l’essentiel pour réussir ton examen en Algorithmique 1.