Verifikation

Betrachte Aussagen der Form {V} P {N} für

• Aussagen V, N (Vor- und Nachbedingung)
• Programm P

,,wenn V gilt, und P ausgeführt wird, gilt danach N ``

Beispiel: {x < 0 und y > 0} x = y - x; {x > 0}

Frage: was ist die schwächste Vorbedingung V, so daß { V } x = y - x; {x > 0}?

Antwort (geraten): y > x.

Aus tatsächlicher Vorbedingun x < 0 und y > 0 folgt y>x, also ist o. g. Beispiel-Aussage wahr.

Statt raten: rechnen mit Regeln.