Correctheidsbewijs
- 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.
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
- 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)
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
- 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
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 !=
Verder zou ik het algoritme zelf nog aanpassen: in de while-lus zou ik
Code: Selecteer alles
while(a < r.Length)
"Als je niet leeft zoals je denkt, zul je snel gaan denken zoals je leeft."
--Vladimir Lenin-- (Владимир Ильич Ульянов)
--Vladimir Lenin-- (Владимир Ильич Ульянов)
- Berichten: 4
Re: Correctheidsbewijs
Ok, bedankt Vladimir.
Maar zou iemand kunnen kijken of het bewijs juist is?
Avast bedankt
Maar zou iemand kunnen kijken of het bewijs juist is?
Avast bedankt
"A man chooses, a slave obeys." Andrew Ryan