Hoaren logiikkaa

Kokeneet kirjoittajat eivät ole vielä tarkistaneet sivun nykyistä versiota, ja se voi poiketa merkittävästi 15.6.2021 tarkistetusta versiosta . tarkastukset vaativat 2 muokkausta .

Hoare-logiikka ( eng. Hoare logic , myös Floyd-Hoare logic tai Hoare-säännöt ) on muodollinen järjestelmä , jossa on joukko loogisia sääntöjä, jotka on suunniteltu todistamaan oikeellisuus tietokoneohjelmat . Sitä ehdotti vuonna 1969 englantilainen tietojenkäsittelytieteilijä ja matemaattinen logiikka Hoare , jonka myöhemmin kehitti Hoare itse ja muut tutkijat. [1] Alkuperäisen idean ehdotti Floyd , joka julkaisi samanlaisen järjestelmän [2 ] , jota sovelletaan vuokaavioihin .

Hoare kolmoset

Hoaren logiikan pääominaisuus on Hoaren kolmois . _ Kolmiosa kuvaa kuinka koodinpalan suoritus muuttaa laskennan tilaa. Hoare-kolmiolla on seuraava muoto:

\{P\}\;C\;\{Q\}

missä P ja Q ovat väitteitä ja C on komento . _ _ _ P :tä kutsutaan ennakkoehdoksi ( antecedent ) ja Q : ta jälkiehdoksi ( seuraus ). Jos ennakkoehto on tosi, komento tekee jälkiehdon tosi. Lausekkeet ovat predikaattilogiikan kaavoja .

Hoaren logiikassa on aksioomat ja päättelysäännöt kaikille yksinkertaisen pakottavan ohjelmointikielen konstrukteille . Näiden Hoaren alkuperäisessä työssä kuvattujen konstruktien lisäksi Hoare ja muut kehittivät sääntöjä muille rakenteille: samanaikainen suoritus , proseduurikutsu , hyppy ja osoitin .

Hoaren pääideana on antaa jokaiselle imperatiivisen kielen konstruktiolle esi- ja jälkiehto , joka on kirjoitettu loogisena kaavana. Siksi nimessä esiintyy kolmois - ennakkoehto , kielirakenne, jälkiehto .

On selvää, että tyhjällä operaattorilla esi- ja jälkiehdot ovat samat.
Jälkiehdossa olevan osoitusoperaattorin osalta on otettava huomioon edellytyksen lisäksi se, että muuttujan arvo on muuttunut.
Yhdistelmälausekkeelle ( Pythonissa se on sisennys, C :ssä se on {} ) meillä on ketju esi- ja jälkiehtoja . Tämän seurauksena ensimmäinen ennakkoehto ja viimeinen jälkiehto voidaan jättää yhdistelmälauseeseen .
Päättelysääntö sanoo, että voimme vahvistaa ennakkoehtoa ja heikentää jälkiehtoa , jos tarvitsemme sitä. Ei ole mitään järkeä pitää koko ohjelmassa jonkinlaista lausuntoa, joka ei auta ratkaisemaan ongelmaa.
Sivuliikeilmoitus tai vain jos . Se voidaan jakaa ehdollisesti kahteen haaraan: then ja else . Jos lisätään loogisen ehdon totuus ennakkoehtoon (mikä on if :n alla), niin sitten haaran suorittamisen jälkeen tulee seurata jälkiehto . Vastaavasti, jos lisäämme loogisen ehdon negaation ennakkoehtoon (mikä on if :n alla), niin else - haaran suorituksen jälkeen tulee seurata jälkiehto
silmukan operaattori. Tämä on ei-triviaalisin ja monimutkaisin, koska silmukka voidaan suorittaa monta kertaa, eikä se edes pääty. Silmukan rungon mahdollisen toistuvan toiston ongelman ratkaisemiseksi otetaan käyttöön silmukkainvariantti . Silmukan invariantti on jotain, joka on tosi ennen sen suorittamista, on totta jokaisen silmukan rungon suorituksen jälkeen ja on siten totta silmukan lopun jälkeen. Silmukkakäskyn edellytys on yksinkertaisesti sen silmukan invariantti . Jos silmukan jatkuvuusehto on tosi (mikä on alle while ), niin silmukan rungon suorittamisen jälkeen silmukan invariantin totuuden tulisi seurata . Tämän seurauksena meillä on syklin päätyttyä jälkiehtona syklin invariantin totuus ja syklin jatkamisen ehdon negaatio.
Silmukkaoperaattori täysin oikein. Tätä varten edelliseen kappaleeseen lisätään rajoittava funktio, jonka avulla on helppo todistaa, että silmukka suoritetaan rajoitetun määrän kertoja. Sille asetetaan ehdot, että se on aina >=0, pienenee tiukasti jokaisen silmukan rungon suorituksen jälkeen ja tarkalleen = 0 silmukan päättyessä.

Hyvin toimiva ohjelma voidaan kirjoittaa monella tapaa ja monissa tapauksissa se on tehokas. Tämä epäselvyys vaikeuttaa ohjelmointia. Voit tehdä tämän esittelemällä tyylin. Mutta tämä ei riitä. Monien ohjelmien (esimerkiksi epäsuorasti ihmisten elämään liittyvien) kohdalla on myös tarpeen todistaa niiden oikeellisuus. Kävi ilmi, että oikeellisuustodistus tekee ohjelman kalliimmaksi suuruusluokkaa (noin 10 kertaa).

Osittainen ja täydellinen oikeellisuus

Hoaren standardilogiikassa vain osittainen oikeellisuus voidaan todistaa, koska ohjelman lopettaminen on todistettava erikseen. Myöskään sääntöä olla käyttämättä redundantteja ohjelman osia ei voida ilmaista Hoaren logiikassa. "Intuitiivinen" ymmärrys Hoaren kolmiosta voidaan ilmaista seuraavasti: jos P esiintyy ennen kuin C on valmis, joko Q tapahtuu tai C ei koskaan pääty. Itse asiassa, jos C ei pääty, ei ole jälkiä, joten Q voi olla mikä tahansa lause. Lisäksi voimme valita Q :n epätosi osoittamaan, että C ei koskaan pääty.

Täysi oikeellisuus voidaan myös todistaa käyttämällä While -lauseen säännön laajennettua versiota .

Säännöt

Tyhjä operaattoriaksiooma

Tyhjän käskyn sääntö sanoo, että skip -käsky ( tyhjä lause ) ei muuta ohjelman tilaa, joten lause, joka oli tosi ennen ohitusta , pysyy tosi sen suorittamisen jälkeen.

{\displaystyle {\frac {}{\{P\}\ {\textbf {skip}}\ \{P\))))

Tehtäväoperaattorin aksiooma

Tehtäväoperaattorin aksiooma toteaa, että osoituksen jälkeen minkään predikaatin arvo tehtävän oikean puolen suhteen ei muutu, kun oikea puoli korvataan vasemmalla:

{\displaystyle {\frac {}{\{P[E/x]\}\ x:=E\ \{P\))))

Tässä tarkoitetaan lauseketta P , jossa kaikki vapaan muuttujan x esiintymät korvataan lausekkeella E . $P[E/x]$

Tehtäväaksiooman tarkoitus on, että totuus on ekvivalentti tehtävän suorittamisen jälkeen. Siten, jos se oli tosi ennen tehtävää, tehtävän aksiooman mukaan se on totta tehtävän jälkeen. Päinvastoin, jos se oli yhtä suuri kuin "false" ennen määrityslauseketta, sen pitäisi olla yhtä suuri kuin "false" sen jälkeen. $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$

Esimerkkejä kelvollisista kolmioista:

${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\))$
${\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\))$

Hoaren muotoilun osoitusaksiooma ei päde , kun useampi kuin yksi tunniste viittaa samaan arvoon. Esimerkiksi,

\{ y = 3\} \ x := 2\ \{y = 3 \}

on epätosi, jos x ja y viittaavat samaan muuttujaan, koska mikään ennakkoehto ei voi varmistaa, että y on 3 sen jälkeen, kun x :lle on annettu 2.

Koostumussääntö

Hoaren kokoonpanosääntö pätee ohjelmien S ja T peräkkäiseen suoritukseen , jossa S suoritetaan ennen T :tä, joka kirjoitetaan S;T :llä .

{\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{ R\}}}

Tarkastellaan esimerkiksi kahta tehtävän aksiooman esiintymää:

\{ x + 1 = 43\} \ y := x + 1\ \{y =43 \}

\{ y = 43\} \ z := y\ \{z = 43 \}

Koostumussäännön mukaan saamme:

\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z = 43 \}

Ehdollinen operaattorin sääntö

{\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\ }\ {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}

Päättelysääntö

{\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime )){\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}

Silmukkalauseen sääntö

{\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S \ {\textbf {done}}\ \{\neg B\wedge P\}}}

Tässä P on sykliinvariantti .

Kierrä lauseen sääntö täysin oikein

{\frac {<\;{\text{on perusteltu,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P] \ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ [\neg B\wedge P]}}

Tässä säännössä silmukan invariantin säilyttämisen lisäksi silmukan päättyminen todistetaan termillä, jota kutsutaan silmukkamuuttujaksi (tässä t ), jonka arvoa pienennetään tiukasti perustellun suhteen " < " mukaisesti jokaisella iteraatiolla. Tässä tapauksessa ehdon B tulee viitata siihen, että t ei ole alueensa vähimmäiselementti, muuten tämän säännön lähtökohta on väärä. Koska " < "-relaatio on täysin perusteltu, jokainen silmukan vaihe määritellään äärellisen lineaarisesti järjestetyn joukon pienenevillä jäsenillä .

Tämän säännön merkinnöissä käytetään hakasulkeita, ei kiharoita, osoittamaan säännön täydellistä oikeellisuutta. (Tämä on yksi tapa osoittaa täydellistä oikeellisuutta.)

Esimerkkejä

Esimerkki 1

{\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\))

— tehtävän aksiooman perusteella.

Koska päättelysäännön perusteella saamme:

( x + 1 = 43 \nuoli vasen oikealle x = 42)

\{x=42\}\ y:=x+1\ \{y=43\land x=42\}

Esimerkki 2

{\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\))

— tehtävän aksiooman perusteella.

Jos x ja N ovat kokonaislukuja, niin , ja päättelysäännön perusteella saadaan:

(x < N) \tarkoittaa (x+1 \leq N)

{\displaystyle \{x<N\}\ x:=x+1\ \{x\leq N\))

Katso myös

Linkit

↑ CAR Hoare . " Aksiomaattinen perusta tietokoneohjelmointiin Arkistoitu 17. heinäkuuta 2011 Wayback Machinessa ". ACM:n tiedonannot , 12(10):576-580,583, lokakuu 1969. doi : 10.1145/363235.363259
↑ RW Floyd . « Sanojen antaminen ohjelmille. Arkistoitu alkuperäisestä 9. joulukuuta 2008. (downlink alkaen 13-05-2013 [3444 päivää] - historia ) » (ladattu linkki) Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Voi. 19, s. 19-31. 1967.

Kirjallisuus

Guts AK Matemaattinen logiikka ja algoritmien teoria. - M . : Kirjatalo "LIBROKOM", 2009. - 117 s. — ISBN 9785397000567 .
https://web.archive.org/web/20110123200456/http://djvu-student.narod.ru/02-matematicheskaya-logika/metodichka/metoda_matlogika_i_teor_algoritm_g6.html

Bibliografisissa luetteloissa	GND : 4343105-7