Schleifenregel

{ P } while B do C { Q }

In einem Rückwärts-Beweis muß eine geeignete

Invariante I geraten werden !

Der Beweis einer Schleife benötigt eine Invariante I

P Þ I

{ I Ù B } C { I }

I Ù Ø B Þ Q

anfangs ist I wahr

I wird in der Schleife erhalten

am Schluß garantiert I

die Nachbedingung

I

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen