Correctheidsbewijs

Moderators: jkien, Xilvo

Reageer
Gebruikersavatar
Berichten: 4

Correctheidsbewijs

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.
"A man chooses, a slave obeys." Andrew Ryan

Gebruikersavatar
Berichten: 4

Re: Correctheidsbewijs

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)
"A man chooses, a slave obeys." Andrew Ryan

Gebruikersavatar
Berichten: 829

Re: Correctheidsbewijs

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 !=
"Als je niet leeft zoals je denkt, zul je snel gaan denken zoals je leeft."

--Vladimir Lenin-- (Владимир Ильич Ульянов)

Gebruikersavatar
Berichten: 4

Re: Correctheidsbewijs

Ok, bedankt Vladimir.

Maar zou iemand kunnen kijken of het bewijs juist is?

Avast bedankt
"A man chooses, a slave obeys." Andrew Ryan

Reageer