Formale Verifikation - Aufgaben

Aufgabe:  (Abwärts zählen bis 0 – partielle und totale Korrektheit)

Gegeben sei folgende While-Schleife W mit Schleifen­körper S:

while (i>0)
    i=i-1;

Beweisen Sie {P} W {R} mit R: i = 0 im Sinne der totalen Korrektheit. Wie lautet die schwächste Vorbedingung P?