Loopinvariant

En loopinvariant är ett enkelt men ändå kraftfullt verktyg för att bättre förstå slingor (while- och for-satser). En väl vald loopinvariant är till nytta både när man skriver programmet, när man testar det och när man modifierar det. En loopinvariant fungerar dessutom som dokumentation och kan utgöra grunden för ett korrekthetsbevis.

Exempel 1: summa

Ett enkelt exempel får illustrera hur loopinvarianter fungerar.

// Sum returns the sum 1 + 2 + ... + n, where n ≥ 0.
func Sum(n int) int64 {
    var sum int64
    i := 1
    for i <= n {
        // Invariant: sum = 1 + 2 + ... + (i - 1)
        sum += int64(i)
        i++
    }
    return sum
}

En invariant är ett påstående om variablerna i ett program som är sant varje gång programmet passerar invarianten. I det här avsnittet kommer vi speciellt att titta på loopinvarianter: invarianter som står i början (eller slutet) av en slinga. En bra loopinvariant har följande tre egenskaper.

De tre stegen ovan är i själva verket ett induktionsbevis som visar att sum = 1 + 2 + ... + n när programmet lämnar slingan.

Exempel 2: max

I nästa exempel använder vi en loopinvariant redan när vi designar algoritmen. Vi börjar med följande kodskelett.

// Max returns the maximum value in v.
func Max(v []int) int {
    max := …
    for i := 0; i < len(v); i++ {
        // Invariant: max = max(v[0], v[1], ..., v[i-1])
        …
    }
    return max
}

Invarianten verkar vara väl vald: den uppfyller ju den tredje egenskapen (avslutning) eftersom den säger att variabeln max = max(v[0], v[1], ..., v[len(v)-1]) när slingan avslutas.

Den första egenskapen (initiering) kan vi försöka uppfylla genom att att tilldela max ett lämpligt startvärde. Det visar sig svårt eftersom det är oklart hur man definierar maxvärdet av en tom vektor. Vi har hittat en potientiell bugg i programmet redan innan vi har skrivit koden! Det finns flera lösningar. Jag väljer att ändra metodens kontrakt:

// Max returns the maximum value in v.
// It panics if len(v) is 0.
func Max(v []int) int {
    if len(v) == 0 {
        panic("len(v) == 0")
    }
    max := …
    for i := 0; i < len(v); i++ {
        // Invariant: max = max(v[0], v[1], ..., v[i-1])
        …
    }
    return max
}

Nu är det lätt all lösa problemet. Om vi låter max = v[0] och startar slingan med i = 1 så är loopinvarianten uppfylld första gången vi kommer in i slingan.

Nu återstår bara att skriva koden inuti slingan. När vi gör det så kan vi utgå från att loopinvarianten gäller i början av slingan. Egenskap två (uppdatering) säger nämligen: Om invarianten är sann i en iteration av slingan så måste den vara sann även i nästa iteration. Den färdiga metoden ser då ut så här.

// Max returns the maximum value in v.
// It panics if len(v) is 0.
func Max(v []int) int {
    if len(v) == 0 {
        panic("len(v) == 0")
    }
    max := v[0]
    for i := 1; i < len(v); i++ {
        // Invariant: max = max(v[0], v[1], ..., v[i-1])
        if v[i] > max {
            max = v[i]
        }
    }
    return max
}

Exempel 3: insättningssortering

// Sort reorders the elements of v so that
// v[0] ≤ v[1] ≤ … ≤ v[len(v)-1].
func Sort(v []int) {
    for j := 1; j < len(v); j++ {
        // Invariant: v[0:j-1] contains the same elements as
        // the original vector v[0..j-1], but in sorted order.
        key := v[j]
        i := j - 1
        for i >= 0 && v[i] > key {
            v[i+1] = v[i]
            i--
        }
        v[i+1] = key
    }

}

För att uppnå egenskap tre (avslutning) så behöver vi en loopinvariant som säger att elementen är sorterade och att det dessutom är samma element som i ursprungsvektorn.

Vi börjar med att kontrollera den första egenskapen (initiering). Vi kan anta att vektorn innehåller minst två element eftersom for-loopen annars inte exkeveras. (Det behövs inte heller eftersom en vektor med 0 eller 1 element alltid är sorterad.) Innan slingan exekveras säger loopinvarianten att "delvektorn v[0..1-1] består av samma element som ursprungsvektorn v[0..1-1] men i sorterad ordning." Detta påstående är sant.

För att verifiera egenskap två (uppdatering) måste vi titta lite närmre på koden. Vi antar att loopinvarianten håller (dvs v[0..j-1] är sorterad) och behöver bara kontrollera att koden sätter in elementet v[j] på rätt plats i delvektorn v[0..j]. Detta sker genom att man flyttar alla element v[j-1], v[j-2],... som är större än v[j] ett steg till höger och därefter sätter in v[j] på sin rätta plats.

Om man vill så kan man naturligtvis använda en loopinvariant även för att kontrollera att koden i while-loopen är korrekt. Det kan vara en bra övning.

Stefan Nilsson