Correctheidsbewijs

[Andrew Ryan]

Hallo,

Ik moet al oefening een correctheidsbewijs opstellen voor een programma dat uit een rij de maximale deelrijsom berekend.

De programmeertaal is java.

public int maxSomV3()

int maximum = 0; int maxtotgrens = 0;

int a =0;

while( a!= r.lenght)

{ maxtotgrens = Math.max(0, maxtotgrens+r[a]);

maximum = Math.max( maximum, maxtotgrens);

a++;

}

return maximum;

}

Ik heb al gedacht om de invariant in deze vorm te schrijven : maximum = Math.max( maximum , Math.max(0,maxtotgrens+r[a]))

Maar ik zie niet in hoe ik het zou moeten bewijzen.

Alle hulp is alvast welkom.

[Andrew Ryan]

Ik denk dat ik het gevonden heb.

Invariant: P = Math.max(maximum,maxtotgrens).

mogelijke uitwerkingen :

1)

P=Math.max(maximum, Math.max(0,maxtotgrens+r[a])) { Math.max(0,maxtotgrens) , maxtotgrens+r[a] <0}

P= Math.max(Math.max(maximum, maxtotgrens),0) ) { maximum is altijd groter of gelijk aan 0}

P= Math.max(maximum,maxtotgrens)

2)

P=Math.max(maximum, Math.max(0,maxtotgrens+r[a])) { Math.max(0,maxtotgrens) , maxtotgrens+r[a] >0}

P= Math.max(Math.max(maximum, maxtotgrens),maxtotgrens+r[a]) ) { maximum is altijd groter of gelijk aan 0}

P= Math.max(Math.max(maximum, maxtotgrens),maxtotgrens+r[a-1]) ) { a-1 komt door a++}

P= Math.max(maximum,maxtotgrens)

[Vladimir Lenin]

Het bewijs van een lusinvariant kan je eigenlijk opvatten als een bewijs van volledige inductie. Je schrijft dus je lusinvariant op, vervolgens bewijs je eerst dat hij bij het begin van de lus (vooraleer hij de eerste keer erdoor gaat waar is). Dat zou je als de basisstap kunnen zien, vervolgens dien je dus te bewijzen uit de vorige stap, dat na een volgende draai door de lus, de invariant nog steeds klopt, dat is dus de inductiestap van het bewijs met volledige inductie. Hou er wel rekening mee dat je bij lussen ook een eindigheidsbewijs dient op te stellen. Dit bewijst dat er vroeg of laat een moment zal zijn waarop de lus zal stoppen.

Verder zou ik het algoritme zelf nog aanpassen: in de while-lus zou ik

Code: Selecteer alles

while(a < r.Length)

schrijven. Dat is een sterkere conditie, uiteraard is dit algoritme af, maar stel dat iemand die a++ zou omzetten in a += 3; dan zou je problemen kunnen krijgen. Er wordt aangeraden om bij algoritmes steeds sterke condities te gebruiken. Dit is dus <, <=, >, >= en niet == of !=

[Andrew Ryan]

Ok, bedankt Vladimir.

Maar zou iemand kunnen kijken of het bewijs juist is?

Avast bedankt