Loop invariantti

Loop invariant  - ohjelmoinnissa  - looginen lauseke , joka on tosi jokaisen silmukan rungon läpimenon jälkeen (kiinteän operaattorin suorittamisen jälkeen ) ja ennen silmukan alkua, riippuen silmukan rungossa muuttuvista muuttujista. [1] Invariantteja käytetään ohjelman verifioinnin teoriassa todistamaan syklisellä algoritmilla saadun tuloksen oikeellisuus.

Määritelmä

Silmukan invariantti on matemaattinen lauseke (yleensä yhtälö), joka sisältää väistämättä ainakin joitain muuttujia, joiden arvot muuttuvat silmukan iteraatiosta toiseen. Invariantti konstruoidaan siten, että se on tosi välittömästi ennen silmukan suorituksen alkua (ennen ensimmäiseen iteraatioon pääsyä) ja jokaisen iteroinnin jälkeen. Lisäksi, jos invariantissa on vain syklin sisällä määritettyjä muuttujia (esimerkiksi syklilaskuri Pascalissafor tai Adassa ) , syklin syöttämiseksi ne otetaan huomioon arvoilla, jotka ne saavat alustuksen yhteydessä.

Todiste silmukan oikeellisuudesta käyttämällä invarianttia

Menettely syklin toimivuuden osoittamiseksi invariantin avulla on seuraava:

  1. On todistettu, että invariantin lauseke on tosi ennen syklin alkua.
  2. On todistettu, että invariantin lauseke pysyy totta silmukan rungon suorittamisen jälkeen; siten induktiolla todistetaan, että koko syklin lopussa invariantti täyttyy.
  3. On todistettu, että jos invariantti on tosi, silmukan päättymisen jälkeen muuttujat ottavat täsmälleen ne arvot, jotka vaaditaan saamaan (tämä määräytyy alkeellisesti invariantin lausekkeesta ja tunnetuista lopullisista arvoista muuttujat, joihin silmukan päättämisen ehto perustuu).
  4. Todistetaan (ehkä käyttämättä invarianttia), että sykli päättyy, eli lopetusehto täyttyy ennemmin tai myöhemmin.
  5. Edellisissä vaiheissa todistettujen lausuntojen totuus osoittaa yksiselitteisesti, että silmukka suoritetaan äärellisessä ajassa ja antaa halutun tuloksen.

Invariantteja käytetään myös syklisten algoritmien suunnittelussa ja optimoinnissa . Esimerkiksi sen varmistamiseksi, että optimoitu silmukka pysyy oikeana, riittää, kun todistetaan, että silmukan invarianttia ei rikota ja silmukan lopetusehto on saavutettavissa.

Muistiinpanot

  1. ↑ V.V. Borisenko. Ohjelmoinnin perusteet (linkki ei saatavilla) . TIEDÄ Intuit . Haettu 18. kesäkuuta 2013. Arkistoitu alkuperäisestä 20. toukokuuta 2012.