Hoare Logic: Fondements et applications

Cette séance de cours fournit une exploration approfondie de Hoare Logic, un système formel de raisonnement sur l'exactitude des programmes informatiques. Il commence par un examen de différentes sémantiques, y compris la sémantique opérationnelle, dénotationnelle et axiomatique, en soulignant le rôle des assertions dans la définition des propriétés du programme. L'instructeur discute du contexte historique de Hoare Logic, en soulignant son développement par des pionniers tels que Floyd et Dijkstra. La séance de cours couvre la définition de l'exactitude partielle et totale, illustrant ces concepts avec des exemples et des quiz. L'instructeur explique l'importance des conditions préalables et postconditions dans les spécifications du programme, démontrant comment établir la validité par des règles de preuve. La séance de cours présente également la syntaxe et les règles de Hoare Logic, y compris les règles d'affectation, de séquençage, de conditionnalités et de boucles. La validité et l'exhaustivité de la logique sont discutées, ainsi que ses applications dans la vérification des programmes et le raisonnement sur les programmes impératifs. La session se termine par une discussion sur les limites de Hoare Logic et l'émergence de la logique de séparation comme une approche plus modulaire du raisonnement sur l'exactitude du programme.