Programm Verifizerer

{ P }

S

{ Q }

Programm-

verifizierer

p1 Þ q1

.....

pn Þ qn

annotatiert mit

- Vorbedingung,

- Nachbedingung

- Schleifeninvarianten

Logische

Implikationen

“Verifikations-

bedingungen”

Verifikations-

bedingungen

Programm

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen