Wetenschapsforum

Hey,

even een vraagje over correctheidsbewijzen van algoritmes.

Als je het correctheidsbewijs moet opstellen voor 2 (of meerdere) while lussen die in elkaar genest zijn, moet je dan een invariant bepalen voor het geheel alleen, of ook nog een aparte invariant voor de geneste lus?

Voor elke lus.

merci

Voor de buitenste lus mag je aannemen dat als voor de aanroep de preconditie geldt dan moet na de aanroep de postconditie geldig zijn, maw je kunt de binnenste lus beschouwen als een procedure aanroep. Je moet daarom beide afzonderlijk bewijzen.