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.