Springen naar inhoud

Correctheidsbewijs


  • Log in om te kunnen reageren

#1

Andrew Ryan

    Andrew Ryan


  • 0 - 25 berichten
  • 4 berichten
  • Gebruiker

Geplaatst op 31 juli 2009 - 14:04

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

Dit forum kan gratis blijven vanwege banners als deze. Door te registeren zal de onderstaande banner overigens verdwijnen.

#2

Andrew Ryan

    Andrew Ryan


  • 0 - 25 berichten
  • 4 berichten
  • Gebruiker

Geplaatst op 31 juli 2009 - 14:39

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

#3

Vladimir Lenin

    Vladimir Lenin


  • >250 berichten
  • 829 berichten
  • Ervaren gebruiker

Geplaatst op 31 juli 2009 - 14:42

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
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 !=

Veranderd door Vladimir Lenin, 31 juli 2009 - 14:44

"Als je niet leeft zoals je denkt, zul je snel gaan denken zoals je leeft."
--Vladimir Lenin-- (Владимир Ильич Ульянов)

#4

Andrew Ryan

    Andrew Ryan


  • 0 - 25 berichten
  • 4 berichten
  • Gebruiker

Geplaatst op 31 juli 2009 - 15:28

Ok, bedankt Vladimir.

Maar zou iemand kunnen kijken of het bewijs juist is?

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





0 gebruiker(s) lezen dit onderwerp

0 leden, 0 bezoekers, 0 anonieme gebruikers

Ook adverteren op onze website? Lees hier meer!

Gesponsorde vacatures

Vacatures