Archief - Correctheidsbewijs Maximale Deelrijsom (Java)

Het archief is een bevroren moment uit een vorige versie van dit forum, met andere regels en andere bazen. Deze posts weerspiegelen op geen enkele manier onze huidige ideeën, waarden of wereldbeelden en zijn op sommige plaatsen gecensureerd wegens ontoelaatbaar. Veel zijn in een andere tijdsgeest gemaakt, al dan niet ironisch - zoals in het ironische subforum Off-Topic - en zouden op dit moment niet meer gepost (mogen) worden. Toch bieden we dit archief nog graag aan als informatiedatabank en naslagwerk. Lees er hier meer over of start een gesprek met anderen.
c

cypres

Legacy Member
Beste mede-9livers, :help:

Ik heb vrijdag examen Methodiek van de Informatica (KUL van P. Dutré).
Hierbij wordt altijd dezelfde vraag gesteld die geen van mijn mede-burgies (die ik ken allesinds) al heeft kunnen oplossen:

Namelijk het correctheidsbewijs/ of enkel de invariant dat ditvolgende stukje programma bewijst:

Met r een array van getallen

Code: 
public int maxdeelrijsom() {

int maximum = 0, maxtotgrens = 0, a =0;

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

maximum = Math.max(maximum, maxtotgrens);

a++

}

return maximum;

}

Als iemand de invariant / correctheidsbewijs weet/kan vinden, 1000 maal dank! ik heb mij er al dood op geergerd.

Tot nu toe dacht ik aan:

invariant ==> a < r.length && maximum >= maxtotgrens && maxtotgrens = Math.max(0, (sommatie van x => a van r[x])) && x is element van [0,a-1]



Ik zou zeggen Have fun, alvast bedankt!!

:applause::applause:
n

nguaroth

Legacy Member
Dit lijkt me niet moeilijk, je invariante betrekkingen lijken goed te zijn.
duid punten in je programma eens aan met nummertjes, maak dan een flow chart van je programma aan de hand van deze nummers en bewijs de direct na elkaar liggende punten in dit programma. Als je hier mee alle invariante betrekkingen kan aantonen, is je bewijs normaal compleet,

Moest het echt niet lukken kan je het altijd opnieuw vragen en dan zal ik u wel een oplossing geven:)

Het is eigenlijk gewoon veel schrijf werk, echt moeilijk is dat niet.
N

NeverwinterX

Legacy Member
Ik neem aan dat er nog een a++; moet komen onderin de while? (Anders is het nogal triviaal en is het algoritme niet correct want het gaat in oneindige lus :p)
Gebruik code tags in het vervolg.
Dit is het algoritme waarover het gaat trouwens: Maximum subarray problem - Wikipedia, the free encyclopedia

De invariant van de while loop is dat telkens de loop beneden komt dat 'maximum' de maximale som van de subarrays van de array tot positie 'a' of lager bevat. Op het einde van de hele while loop is 'a' gelijk aan de lengte van de array en bevat 'maximum' het gewenste resultaat. (Bijkomend is dat 'maxtotgrens' telkens de loop beneden komt de maximale som van de subarrays van de array die eindigen op positie 'a' bevat.)

zeg tegen Dutré trouwens eens dat hij mijn mail moet beantwoorden :p
c

cypres

Legacy Member
nguaroth zei:
Dit lijkt me niet moeilijk, je invariante betrekkingen lijken goed te zijn.
duid punten in je programma eens aan met nummertjes, maak dan een flow chart van je programma aan de hand van deze nummers en bewijs de direct na elkaar liggende punten in dit programma. Als je hier mee alle invariante betrekkingen kan aantonen, is je bewijs normaal compleet,

Moest het echt niet lukken kan je het altijd opnieuw vragen en dan zal ik u wel een oplossing geven:)

Het is eigenlijk gewoon veel schrijf werk, echt moeilijk is dat niet.
Klik om te vergroten...

Als je kan zeggen dat mijn invariant idd volledig correct is, is het correctheidsbewijs echt peanuts! Ik was op het examen vergeten de x te definiëren. Hierbij gaf de prof mij 0/4 voor de oefening, ookal had ik ook de eindigheid en al de andere deelvragen correct==> resultaat 9,8/20: Hurraay!

NeverwinterX zei:
Ik neem aan dat er nog een a++; moet komen onderin de while? (Anders is het nogal triviaal en is het algoritme niet correct want het gaat in oneindige lus :p)
Gebruik code tags in het vervolg.
Dit is het algoritme waarover het gaat trouwens: Maximum subarray problem - Wikipedia, the free encyclopedia

De invariant van de while loop is dat telkens de loop beneden komt dat 'maximum' de maximale som van de subarrays van de array tot positie 'a' of lager bevat. Op het einde van de hele while loop is 'a' gelijk aan de lengte van de array en bevat 'maximum' het gewenste resultaat. (Bijkomend is dat 'maxtotgrens' telkens de loop beneden komt de maximale som van de subarrays van de array die eindigen op positie 'a' bevat.)

zeg tegen Dutré trouwens eens dat hij mijn mail moet beantwoorden :p
Klik om te vergroten...

a++ en code: done!

vrijdag zal hij wrs wel iets komen zeggen in den aula! Ik zal hem zeggen dat hij op NeverWinterX moet antwoorden :D!
n

nguaroth

Legacy Member
Wat neverwinterx aanhaalde is inderdaad waar. Als je dit nu gewoon even schetst zoals ik zei en dan even de stappen stuk per stuk bewijst is het echt peanuts, moest het niet lukken dan laat je het maar weten.
c

cypres

Legacy Member
Het is me volledig gelukt! De invariant die ik had klopte niet volledig want ik nam altijd de som tot het laatste element maar het kon idd zoals neverwinterX een subarray zijn dus moest het de som van x=>y zijn met 0<= x <=y <= a<=r.length
Het archief is een bevroren moment uit een vorige versie van dit forum, met andere regels en andere bazen. Deze posts weerspiegelen op geen enkele manier onze huidige ideeën, waarden of wereldbeelden en zijn op sommige plaatsen gecensureerd wegens ontoelaatbaar. Veel zijn in een andere tijdsgeest gemaakt, al dan niet ironisch - zoals in het ironische subforum Off-Topic - en zouden op dit moment niet meer gepost (mogen) worden. Toch bieden we dit archief nog graag aan als informatiedatabank en naslagwerk. Lees er hier meer over of start een gesprek met anderen.
Terug
Bovenaan