Lógica de Hoare: diferenças entre revisões

'''Lógica de Hoare'''(também conhecida como '''lógica de Floyd–Hoare''' ou '''regras de Hoare''') é um [[sistema formal]] com um conjunto de regras lógicas para um raciocínio rigoroso sobre a [[corretude na computação]]. Proposta em 1969 pelo cientista da computação e [[lógica matemática|lógico]] britânico [[Charles Antony Richard Hoare|C. A. R. Hoare]], e subsequêncialmente aprimradaaprimorada por Hoare e outros pesquisadores.<ref>[[Charles Antony Richard Hoare|C. A. R. Hoare]]. "[http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf An axiomatic basis for computer programming]". ''[[Communications of the ACM]]'', 12(10):576&ndash;580,583 October 1969. {{doi|10.1145/363235.363259}}</ref> A idéia original havia sido idealizada pelo trabalho de [[Robert Floyd]], que publicou um sistema similar<ref>[[Robert Floyd|R. W. Floyd]]. "[http://www.cs.virginia.edu/~weimer/2007-615/reading/FloydMeaning.pdf Assigning meanings to programs.]" Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.</ref> para [[fluxograma]]s.