Hoaren logiikka
Hoaren logiikka (myös Floyd-Hoare -logiikka[1]) tarkoittaa formaalia menetelmää ohjelman oikeellisuuden päättelemiseen.[2] 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.[3][2]
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.[4][5][6]
Lähteet
[muokkaa | muokkaa wikitekstiä]- ↑ Hoare Logic, Part I cs.cornell.edu. Viitattu 29.8.2024. (englanniksi)
- ↑ a b Lecture Notes: Hoare Logic (PDF) cs.cmu.edu. Viitattu 14.8.2024. (englanniksi)
- ↑ Hoare Logic (PDF) cl.cam.ac.uk. Viitattu 29.8.2024. (englanniksi)
- ↑ C. A. R. Hoare: An axiomatic basis for computer programming dl.acm.org. lokakuu 1969. doi:10.1145/363235.363259. Viitattu 29.8.2024. (englanniksi)
- ↑ C. A. R. Hoare & C. B. Jones: Procedures and parameters: an axiomatic approach dl.acm.org. 1989. Viitattu 29.8.2024. (englanniksi)
- ↑ Krzysztof R. Apt & Ernst-Rudiger Olderog: Fifty years of Hoare’s logic (PDF) ir.cwi.nl. Viitattu 29.8.2024. (englanniksi)
Aiheesta muualla
[muokkaa | muokkaa wikitekstiä]- Matematiikan ohjelmointi (PDF)