Partial correctness assertions

{ P } C {Q}

Vorbedingung

Nachbedingung

Programm

Wenn C in einem Zustand s startet in dem P wahr ist, und wenn C terminiert,

dann wird am Ende Q wahr sein.

"s, s’ . [P](s) Ù [C](s)=s’ ¹ ^

Þ

[Q](s’)

Formal:

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen