Logique de hoare
- Logique de hoare
-
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[1]. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. 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 décrit les évolutions possibles de l'état d'un programme informatique. Les évolutions sont modélisées par des règles et l'état d'un programme est symbolisé par un triplet
où P et Q sont des prédicats et C est une commande (une action sur le programme). La condition P est appelée la précondition et Q la postcondition.
La logique de Hoare a des axiomes et des règles d'inférence pour toutes les instructions de base d'un langage de programmation impératif. Hoare rajoute dans son papier originel des règles pour les procédures, les sauts, les pointeurs et la concurrence.
Voir aussi
Références
Portail de l’informatique
Catégorie : Méthode formelle
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Logique de hoare de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
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[1]. La méthode de… … Wikipédia en Français
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[1]. La méthode de… … Wikipédia en Français
Logique De Séparation — La logique de séparation (du terme anglais « Separation Logic »), attribuée à John C. Reynolds, est une extension de la logique de Hoare. Par rapport à cette dernière, elle permet de raisonner plus simplement sur les programmes qui… … Wikipédia en Français
Logique de separation — Logique de séparation La logique de séparation (du terme anglais « Separation Logic »), attribuée à John C. Reynolds, est une extension de la logique de Hoare. Par rapport à cette dernière, elle permet de raisonner plus simplement sur… … Wikipédia en Français
Logique de séparation — La logique de séparation (du terme anglais « Separation Logic »), attribuée à John C. Reynolds, est une extension de la logique de Hoare. Par rapport à cette dernière, elle permet de raisonner plus simplement sur les programmes qui… … Wikipédia en Français
C.A.R. Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Computing … Wikipédia en Français
C.A. Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Compu … Wikipédia en Français
C. A. R. Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Compu … Wikipédia en Français
Charles Antony Richard Hoare — C.A.R. Hoare en 2011. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Computing Laboratory. Il est connu… … Wikipédia en Français
Tony Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Compu … Wikipédia en Français
