Slinga invariant

Loop invariant  - i programmering  - ett logiskt uttryck som är sant efter varje pass av loopkroppen (efter exekveringen av den fasta operatorn ) och före starten av loopen, beroende på de variabler som ändras i loopkroppen. [1] Invarianter används i teorin om programverifiering för att bevisa riktigheten av resultatet som erhålls med en cyklisk algoritm.

Definition

En loopinvariant är ett matematiskt uttryck (vanligtvis en likhet) som oundvikligen inkluderar åtminstone några variabler vars värden ändras från en iteration av loopen till nästa. Invarianten är konstruerad på ett sådant sätt att den är sann omedelbart före starten av slingexekveringen (innan den första iterationen går in) och efter var och en av dess iterationer. Dessutom, om invarianten innehåller variabler som bara definieras i cykeln (till exempel cykelräknaren fori Pascal eller Ada ), för att gå in i cykeln tas de i beaktande med de värden som de kommer att få vid tidpunkten för initiering.

Bevis på slingans korrekthet med hjälp av invarianten

Proceduren för att bevisa cykelns funktionsduglighet med hjälp av en invariant är följande:

  1. Det är bevisat att uttrycket av invarianten är sant före cykelns början.
  2. Det är bevisat att uttrycket av invarianten förblir sant efter exekveringen av loopkroppen; sålunda, genom induktion, är det bevisat att vid slutet av hela cykeln kommer invarianten att vara uppfylld.
  3. Det är bevisat att om invarianten är sann, efter att slingan är avslutad, kommer variablerna att ta exakt de värden som krävs för att erhållas (detta bestäms elementärt från uttrycket av invarianten och de kända slutvärdena för variablerna, på vilka villkoret för att avsluta slingan är baserat).
  4. Det är bevisat (kanske utan att tillämpa invarianten) att cykeln kommer att avslutas, det vill säga att termineringsvillkoret kommer att uppfyllas förr eller senare.
  5. Sanningen i de påståenden som bevisats i de tidigare stegen indikerar otvetydigt att slingan kommer att exekveras på en begränsad tid och kommer att ge det önskade resultatet.

Invarianter används också vid design och optimering av cykliska algoritmer . Till exempel, för att säkerställa att den optimerade slingan förblir korrekt, räcker det att bevisa att slinginvarianten inte kränks och att slingavslutningsvillkoret är uppnåeligt.

Anteckningar

  1. ↑ V.V. Borisenko. Grundläggande programmering (inte tillgänglig länk) . KÄNNA Intuit . Hämtad 18 juni 2013. Arkiverad från originalet 20 maj 2012.