Logique de Hoare
Un article de Wikipédia, l'encyclopédie libre.
Vous avez de 
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 flowcharts de Robert Floyd.
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.
[modifier] Références
- ↑ C. A. R. Hoare.
[pdf] "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. DOI 10.1145/363235.363259
 |
Portail de l'informatique – Accédez aux articles de Wikipédia concernant l’informatique. |
