Hurok invariáns

Hurokinvariáns  - a programozásban  - egy logikai kifejezés , amely a ciklustest minden egyes lépése után (a fix operátor végrehajtása után ) és a ciklus kezdete előtt igaz , attól függően, hogy a ciklustestben milyen változók változnak. [1] Az invariánsokat a programellenőrzés elméletében használják a ciklikus algoritmussal kapott eredmény helyességének bizonyítására .

Definíció

A ciklusinvariáns egy matematikai kifejezés (általában egyenlőség), amely elkerülhetetlenül tartalmaz legalább néhány olyan változót, amelyek értéke a ciklus egyik iterációjáról a másikra változik. Az invariánst úgy állítjuk össze, hogy az igaz legyen közvetlenül a ciklusvégrehajtás kezdete előtt (az első iterációba való belépés előtt) és minden iterációja után. Ezen túlmenően, ha az invariáns csak a cikluson belül definiált változókat tartalmaz (például fora Pascal vagy Ada ciklusszámlálója ), akkor a ciklusba való belépéshez azokat azokkal az értékekkel veszik figyelembe, amelyeket az inicializáláskor kapnak.

A ciklus helyességének bizonyítása az invariáns

A ciklus működőképességének invariáns segítségével történő bizonyításának eljárása a következő:

  1. Bebizonyosodott, hogy az invariáns kifejezése a ciklus kezdete előtt igaz.
  2. Bebizonyosodott, hogy az invariáns kifejezése a ciklustest végrehajtása után is igaz marad; így indukcióval bebizonyosodik, hogy a teljes ciklus végén az invariáns teljesül.
  3. Bebizonyosodott, hogy ha az invariáns igaz, a ciklus befejezése után a változók pontosan azokat az értékeket veszik fel, amelyeket meg kell kapni (ezt alapvetően az invariáns kifejezéséből és az ismert végső értékekből határozzák meg azokat a változókat, amelyeken a ciklus befejezésének feltétele alapul).
  4. Bebizonyosodik (talán az invariáns alkalmazása nélkül), hogy a ciklus véget fog érni, vagyis a befejezési feltétel előbb-utóbb teljesül.
  5. Az előző szakaszokban bizonyított állítások igazságtartalma egyértelműen azt jelzi, hogy a ciklus véges időn belül végrehajtásra kerül, és a kívánt eredményt adja.

Az invariánsokat ciklikus algoritmusok tervezése és optimalizálása során is használják . Például ahhoz, hogy megbizonyosodjunk arról, hogy az optimalizált hurok helyes marad, elég bebizonyítani, hogy a hurokinvariáns nem sérül, és a huroklezárási feltétel teljesíthető.

Jegyzetek

  1. ↑ V.V. Borisenko. A programozás alapjai (nem elérhető link) . ISMERJE Intuit . Letöltve: 2013. június 18. Az eredetiből archiválva : 2012. május 20.