Partielle und totale Korrektheit

• partielle Korrektheit:

  wenn Vorbedingung erfüllt und P ausgeführt wird, dann gilt schließlich Nachbedingung

• totale Korrektheit:

  wenn Vorbedingung gilt, dann ist P tatsächlich komplett ausführbar und es gilt schließlich die Nachbedingung

für Schleifen:

• partielle Korrektheit: ,,Invarianz der Invariante``
• totale Korrektheit: ...außerdem Termination