Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Logique de Hoare
Résumé
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 (récurrence) 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.
Hoare s'est inspiré du travail sur les méthodes formelles dans les organigrammes de Robert Floyd, qui lui n'avait pas eu connaissance des travaux d'Alan Turing sur le sujet.
La logique de Hoare permet de dire comment une portion de code fait évoluer l'état d'un système. Il n'y a pas de liaison précise entre l'état antérieur et l'état postérieur, mais une simple description de l'ensemble des états antérieurs et des états postérieurs, par des prédicats. Cette intuition de transformateur de prédicats est formalisée par la notion de triplet de Hoare : où P et Q sont des prédicats et C est un programme.
Le prédicat P, nommé précondition, décrit l'ensemble des états en entrée de la portion de programme C, tandis que le prédicat Q, nommé postcondition, caractérise un ensemble d'états après transformation par le code C.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.