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

{ I Ù B } C { I }

I wird in der Schleife erhalten

I

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen