Springen naar inhoud

Correctheidsbewijzen


  • Log in om te kunnen reageren

#1

velgrem1989

    velgrem1989


  • >100 berichten
  • 228 berichten
  • Ervaren gebruiker

Geplaatst op 22 juni 2008 - 14:50

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?

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

#2

meijuh

    meijuh


  • >100 berichten
  • 202 berichten
  • Ervaren gebruiker

Geplaatst op 23 juni 2008 - 12:07

Voor elke lus.

#3

velgrem1989

    velgrem1989


  • >100 berichten
  • 228 berichten
  • Ervaren gebruiker

Geplaatst op 23 juni 2008 - 12:39

merci

#4

qrnlk

    qrnlk


  • >5k berichten
  • 5079 berichten
  • Lorentziaan

Geplaatst op 23 juni 2008 - 12:57

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.
Any sufficiently analyzed magic is indistinguishable from science.
Any sufficiently advanced technology is indistinguishable from magic.

There is no theory of protecting content other than keeping secrets – Steve Jobs





0 gebruiker(s) lezen dit onderwerp

0 leden, 0 bezoekers, 0 anonieme gebruikers

Ook adverteren op onze website? Lees hier meer!

Gesponsorde vacatures

Vacatures