Ê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 Graph Search.
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.
Proximité ontologique
Cours associés (2)
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
CS-628: Interactive Theorem Proving CS
A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!
Publications associées (26)
Personnes associées (4)
Concepts associés (13)
Vérification formelle
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
Assertion (software development)
In computer programming, specifically when using the imperative programming paradigm, an assertion is a predicate (a Boolean-valued function over the state space, usually expressed as a logical proposition using the variables of a program) connected to a point in the program, that always should evaluate to true at that point in code execution. Assertions can help a programmer read the code, help a compiler compile it, or help the program detect its own defects.
Analyse statique de programmes
En informatique, la notion d’analyse statique de programmes couvre une variété de méthodes utilisées pour obtenir des informations sur le comportement d'un programme lors de son exécution sans réellement l'exécuter. C'est cette dernière restriction qui distingue l'analyse statique des analyses dynamiques (comme le débugage ou le profiling) qui s'attachent, elles, au suivi de l’exécution du programme. L’analyse statique est utilisée pour repérer des erreurs formelles de programmation ou de conception et pour déterminer la facilité ou la difficulté à maintenir le code.