Loop invariant

Loop invariant  - i programmering  - et logisk udtryk , der er sandt efter hver passage af loop-kroppen (efter udførelsen af ​​den faste operator ) og før starten af ​​loopen, afhængigt af de variabler, der ændres i loop-kroppen. [1] Invarianter bruges i teorien om programverifikation for at bevise rigtigheden af ​​resultatet opnået af en cyklisk algoritme.

Definition

En sløjfe-invariant er et matematisk udtryk (normalt en lighed), der uundgåeligt inkluderer i det mindste nogle variabler, hvis værdier ændres fra en iteration af sløjfen til den næste. Invarianten er konstrueret på en sådan måde, at den er sand umiddelbart før starten af ​​loop-udførelsen (før den første iteration) og efter hver af dens iterationer. Desuden, hvis invarianten inkluderer variabler, der kun er defineret inde i cyklussen (for eksempel cyklustælleren fori Pascal eller Ada ), så tages de i betragtning for at indtaste cyklussen med de værdier, som de vil modtage på initialiseringstidspunktet.

Bevis for løkkens rigtighed ved hjælp af invarianten

Proceduren for at bevise cyklussens funktionsdygtighed ved hjælp af en invariant er som følger:

  1. Det er bevist, at udtrykket af invarianten er sandt før begyndelsen af ​​cyklussen.
  2. Det er bevist, at udtrykket af den invariante forbliver sandt efter udførelsen af ​​løkkelegemet; ved induktion er det således bevist, at ved slutningen af ​​hele cyklussen vil invarianten være opfyldt.
  3. Det er bevist, at hvis invarianten er sand, efter at sløjfen er afsluttet, vil variablerne tage nøjagtigt de værdier, der kræves for at blive opnået (dette bestemmes elementært ud fra udtrykket af invarianten og de kendte endelige værdier af variablerne, som betingelsen for at afslutte sløjfen er baseret på).
  4. Det er bevist (måske uden at anvende invarianten), at cyklussen vil afslutte, det vil sige, at termineringsbetingelsen vil blive opfyldt før eller siden.
  5. Sandheden af ​​de udsagn, der blev bevist i de foregående stadier, indikerer utvetydigt, at løkken vil blive udført i en begrænset tid og vil give det ønskede resultat.

Invarianter bruges også i design og optimering af cykliske algoritmer . For for eksempel at sikre, at den optimerede sløjfe forbliver korrekt, er det nok at bevise, at sløjfe-invarianten ikke er overtrådt, og at sløjfetermineringsbetingelsen er opnåelig.

Noter

  1. ↑ V.V. Borisenko. Fundamentals of Programming (ikke tilgængeligt link) . KEND Intuit . Hentet 18. juni 2013. Arkiveret fra originalen 20. maj 2012.