Formale Verifikation - Aufgaben

Aufgabe:  (Triviale Schleife)

Betrachten Sie folgende While-Schleife W mit Schleifenkörper S:

while (i==0)
    i=1;

Offenbar gilt {true} W {i ≠ 0} im Sinne der partiellen Korrektheit, mit Schleifeninvariante P: true. Geben Sie einen formalen Beweis der totalen Korrektheit.