Smyčka invariantní

Invariant smyčky  - v programování  - logický výraz , který je pravdivý po každém průchodu těla smyčky (po provedení fixního operátoru ) a před začátkem smyčky, v závislosti na proměnných, které se mění v těle smyčky. [1] Invarianty se používají v teorii verifikace programu k prokázání správnosti výsledku získaného cyklickým algoritmem.

Definice

Invariant smyčky je matematický výraz (obvykle rovnost), který nevyhnutelně zahrnuje alespoň některé proměnné, jejichž hodnoty se mění od jedné iterace smyčky k další. Invariant je konstruován tak, aby byl pravdivý bezprostředně před začátkem provádění cyklu (před vstupem do první iterace) a po každé z jeho iterací. Pokud navíc invariant obsahuje proměnné definované pouze uvnitř cyklu (například počítadlo cyklů forv Pascalu nebo Ada ), pak se pro vstup do cyklu berou v úvahu s hodnotami, které obdrží v době inicializace.

Důkaz správnosti smyčky pomocí invariantu

Postup pro prokázání provozuschopnosti cyklu pomocí invariantu je následující:

  1. Je dokázáno, že vyjádření invariantu je pravdivé před začátkem cyklu.
  2. Je dokázáno, že výraz invariantu zůstává pravdivý i po provedení těla smyčky; indukcí je tedy dokázáno, že na konci celého cyklu bude invariant splněn.
  3. Je dokázáno, že pokud je invariant pravdivý, po dokončení cyklu budou proměnné nabývat přesně hodnot, které je třeba získat (to je elementárně určeno z výrazu invariantu a známých konečných hodnot proměnné, na kterých je založena podmínka pro ukončení cyklu).
  4. Je dokázáno (snad bez použití invariantu), že cyklus skončí, tedy že podmínka ukončení bude dříve nebo později splněna.
  5. Pravdivost tvrzení dokázaných v předchozích fázích jednoznačně naznačuje, že smyčka bude provedena v konečném čase a poskytne požadovaný výsledek.

Invarianty se také používají při návrhu a optimalizaci cyklických algoritmů . Například, aby bylo zajištěno, že optimalizovaná smyčka zůstane správná, stačí prokázat, že invariant smyčky není narušen a podmínka ukončení smyčky je dosažitelná.

Poznámky

  1. ↑ V.V. Borisenko. Základy programování (nedostupný odkaz) . POZNAT Intuit . Získáno 18. června 2013. Archivováno z originálu 20. května 2012.