Redigerer Løkkeinvariant

En '''løkkeinvariant''' er innen [[informatikk]] en egenskap ved en [[kontrollflyt|programvareløkke]] som er sann før og etter hver iterasjon. Det er en [[logisk forsikring]], som noen ganger blir sjekket innenfor koden ved hjelp av et [[forsikring (programvareutvikling)|forsikringkall]]. Å kjenne til slike invarianter er viktig for forståelsen av løkkens effekt.

Innenfor [[Verifikasjon (informatikk)|formell programvareverifisering]], spesielt [[Hoarelogikk|Floyd-Hoare tilnærmelsen]], blir løkkeinvarianter uttrykt med en formell [[førsteordens logikk]] og blir brukt for å bevise egenskapene til løkker og ved en utvidelse av [[algoritme]]r som anvender løkkene (vanligvis [[korrekthet (informatikk)|korrekthetsegenskaper]]). Løkkeinvarianter er sanne ved inngangspunktet i hver løkke og i enhver iterasjon, slik at når man forlater løkken vil både løkkeinvariantene og løkkens avslutningstilstand være garantert.

==Litteratur==
* [[Thomas H. Cormen]], [[Charles E. Leiserson]], [[Ronald L. Rivest]], and [[Clifford Stein]]. ''[[Introduction to Algorithms]]'', Second Edition. MIT Press and McGraw-Hill, 2001. {{ISBN|0-262-03293-7}}. Pages 17–19, section 2.1: Insertion sort.
* [[David Gries]]. "A note on a standard strategy for developing loop invariants and loops." ''Science of Computer Programming'', vol 2, pp.&nbsp;207–214. 1984.
* Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. "[http://citeseer.ist.psu.edu/292512.html Dynamically Discovering Likely Program Invariants to Support Program Evolution]." ''International Conference on Software Engineering'', pp.&nbsp;213–224. 1999.
* Robert Paige. "Programming with Invariants." ''IEEE Software'', 3(1):56–69. January 1986.
* Yanhong A. Liu, Scott D. Stoller, and [[Tim Teitelbaum]]. [http://www.cs.sunysb.edu/~stoller/SIEC-SCP.html Strengthening Invariants for Efficient Computation]. ''Science of Computer Programming'', 41(2):139–172. October 2001.
* Michael Huth, Mark Ryan. "Logic in Computer Science.", Second Edition.

{{programmeringsspråk}}
{{Autoritetsdata}}
{{stubb}}

[[Kategori:Programmeringsspråk]]