Løkkeinvariant
En løkkeinvariant er innen informatikk en egenskap ved en 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 forsikringkall. Å kjenne til slike invarianter er viktig for forståelsen av løkkens effekt.
Innenfor formell programvareverifisering, spesielt 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 algoritmer som anvender løkkene (vanligvis 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 rediger
- 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. 207–214. 1984.
- Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. "Dynamically Discovering Likely Program Invariants to Support Program Evolution." International Conference on Software Engineering, pp. 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. 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.