Logique de Hoare

La logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An Axiomatic Basis for Computer Programming. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. Elle est fondée sur la syntaxe en ce sens que la correction d'un programme est décrite et démontrée par induction sur la structure du programme : à chaque règle syntaxique de construction d'un programme correspond une règle de la logique de Hoare. Elle a deux utilisations : fournir un outil de vérification formelle des programmes sans les exécuter (analyse statique), décrire rigoureusement la sémantique des langages de programmation (sémantique axiomatique). La logique de Hoare a des axiomes pour toutes les instructions de base d'un langage de programmation impératif et des règles d'inférence pour les compositions d'instructions comme le si ... alors ... sinon ... ou le tant que. Hoare ajoute dans son article originel des règles pour les procédures, les sauts, les pointeurs et la concurrence.