Hoareannotasjoner

Hoareannotasjoner er en teknikk innen formell programverifikasjon som bruker logiske påstander for å beskrive og bevise riktig oppførsel av imperativ kode. De er basert på Hoare-logikken, som ble introdusert av C. A. R. Hoare i 1969. Gjennom annotasjoner kobles programmets kontrollflyt til formelle betingelser som må være sanne før og etter utførelsen av en del av programmet.

En Hoare-trippel uttrykkes vanligvis som {P} C {Q}, der P er en forutsetning som må være sann før kjøring av kommandoen C, og Q er en ettertilstand som må være sann etter at C har fullført. Delvis riktighet sier at hvis P er sann og C terminerer, så er Q sann etterpå. Total korrekthet legger til at C også må terminere. For komplekse programmer brukes ofte tillegg som invariants for løkker (tilstandssetninger som må være sanne gjennom hele løkken) og en avtakende måleenhet som viser at løkken terminerer.

Annotasjonene inkluderer derfor forutsetninger, ettertilstander og løkkerinvariants, samt ofte en terminering-metrikk (variant) som avtar ved hver iterasjon. Verifikasjonsprosesser omformer annotasjonene til verifikasjonsbetingelser som må bevises enten automatisk av verifikasjonsverktøy eller manuelt av en beviser.

I praksis brukes Hoareannotasjoner i formelle utviklingsmiljøer og i språk med innebygde eller eksterne annotasjonsstøtte, for eksempel verifikasjonsverktøy og spesifikasjonsspråk. De hjelper til å dokumentere intensjonene bak koden og muliggjør bevis for korrekthet, feilkilder og vedlikehold av programvare.

Se også Hoare-logikk, programverifikasjon, pre- og postbetingelser, loopinvariants og verifikasjonsverktøy.