Hoaren logiikka (myös Floyd-Hoare -logiikka) tarkoittaa formaalia menetelmää ohjelman oikeellisuuden päättelemiseen. C. A. R. Hoare esitteli menetelmän osittaiselle oikeellisuuden määrittelylle muodossa {P} C {Q}, jossa C on komento, ja P ja Q ohjelmatilat ennen ja jälkeen komentoa. Hoaren alkuperäinen notaatio käytti muotoa P {C} Q, mutta yleisesti käytetään toista muotoa. Nämä ovat Hoaren triplettejä. Ehdot merkitään matemaattisella notaatiolla loogisien operaatioiden kanssa.
Hoare esitteli käsitteen vuonna 1969 artikkelissa An axiomatic basis for computer programming ja laajensi sitä vuonna 1971 artikkelissa Procedures and parameters: an axiomatic approach. Ensimmäisessä Hoare käsitteli vain yksinkertaisia while-silmukoita, mutta toisessa laajensi myös paikallisiin muuttujiin ja rekursiivisiin proseduureihin.
Lähteet
Aiheesta muualla Matematiikan ohjelmointi (PDF)
Luokka:Tietojenkäsittelytiede