Hoare-Logik
Hoare-Logik dient zur formalen Verifikation von Programmen. Sie beschreibt, welche Bedingungen vor und nach einer Anweisung gelten müssen, um Korrektheit zu garantieren.
{P} X = E {Q}
- Bilden von Q’ durch Ersetzen aller X in Q durch E
- Zeigen, dass P ⇒ Q’ gilt
Für die weakest precondition, basically die Post-Condition nehmen, von unten nach oben überall einsetzen und schauen was rauskommt. Ich habe ein Video dazu aufgenommen, siehe Media > Videos.
Beispiel
if-else Precondition finden
Loop Invariante (Loop Counting)
Slides
Muster erkennen durch Tabellen
Siehe Lecture, Loop Invariant.mp4, Hoare Triples.mp4
Beispielaufgabe zur Invariante (Prüfungsaufgabe)
