Litt om invarianter

Stein Krogdahl Universitetet i Oslo

Magne Haveraaen Universitetet i Bergen

August 1994

1 Innledning

Et begrep som ofte brukes i forbindelse med programmering og verifikasjon av programmer er “invariant”. Dessverre brukes dette begrepet lite i læreboken^{1}. Begrepet anvendes derimot i en del andre kurs ved instituttet, f.eks. i I-220. Vi skal derfor forsøke å gi litt bakgrunn for begrepet her, og siden bruke det utover i kurset der det passer. Vi skal imidlertid ikke legge opp til noe formelt forhold til begrepet, slik man har i I-220.

Når et program utføres vil programmets data hele tiden forandre seg. Om man bare ser på dataene kan disse forandringene virke svært kaotiske, men det finnes selvfølgelig en ide bak programmet, og det er denne som gir mening og system i alle de forandringene som foregår.

Bruk av invarianter er en måte å få slike program-ideer ned på papiret på, og går rett og slett ut på å angi en betingelse eller et utsagn om variabel-verdiene som “alltid” er sant, eller som i hvertfall er sant hver gang programkontrollen passerer utvalgte steder i programmet.

Disse betingelsene vil derfor representere noe som er fast og uforanderlig i en verden som ellers preges av stadige forandringer, derav navnet invarianter. Vi skal nedenfor se på eksempler på noen slike invarianter.

2 Invarianter er ikke avhengig av matematisk formalisme

Invarianter blir ofte uttrykt i nokså matematisk språk som kan være tungt å lese for folk som ikke er vant til slik formalisme. Denne formalismen har imidlertid lite å gjøre med selve ideen med invarianter, og det er derfor fint om man venner seg til å uttrykke invarianter i vanlig språk der man føler at det er naturlig.

2.1 Tre måter å bruke invarianter på

Når man introduserer invarianter presenteres de gjerne som en teknikk for å kunne bevise at et program har visse egenskaper, og mye av omtalen under kommer også til å dreie seg om denne bruken. Når vi bruker invarianter på denne måten må vi imidlertid være svært nøyaktige og komplette (men merk at dette ikke nødvendigvis henger sammen med det å uttrykke seg i matematisk formalisme). Man kan imidlertid også ha nytte av invarianter selv om man ikke er ute etter å lage fullstendige bevis om programmer. De er da en måte å holde fast på hovedideen ved programmet mens man lager det, eller når man skal forsøke å sette seg inn i et allerede ferdigskrevet program. Når man bruker invarianter på denne måten kan man bruke den kompletthetsgrad og det presisjonsnivå man finner hensiktsmessig ut fra situasjonen. Invarianter kan brukes i betraktninger om alle slags programmer, men i vår sammenheng er det tre situasjoner der de er av spesiell

1M.Goodrich & R.Tamassia, Data Structures and Algorithms in JAVA, John Wiley & Sons Inc. 1998