Under forelæsningen blev gennemgået eksempler på korrekthedsbeviser for nedenstående tre eksempler.
A[i] <-> A[w]; w <- w + 1; A[i] <-> A[b]; b <- b + 1;erstattes med
A[i] <-> A[b]; A[b] <-> A[w]; w <- w + 1; b <- b + 1;
ALGORITHM : Majoritet INPUT : Array A af længde n>=1, hvor der findes et majoritets element der forekommer >n/2 gange OUTPUT : x = Majoritet(A) METHOD : i <- 1 j <- 1 x <- A[0] { I } while i < n do if j=0 then x <- A[i] j <- 1 else if x=A[i] then j <- j+1 else j <- j-1 i <- i+1 Invarianten I er: 1) 1 <= i <= n 2) 0 <= j 3) -j <= i - 2 * (antal forekomster af x i A[0]...A[i-1]) 4) for alle y<>x: j <= i - 2 * (antal forekomster af y i A[0]...A[i-1])