HackMD
Academia Sinica IIS Intern [Learning] - Hoare Logic
D
Hoare triples
- {P} C {Q}
- P : 執行前要滿足的狀態
- Q : 執行後要滿足的狀態
- C : 要執行的程式
- state 的定義
Partial and Total Correctness
Partial Correctness
- {P} C {Q} is true if
- whenever C is executed in a state satisfying P
- and if the execution of C terminates
- then the state in which C's execution terminates satisfies Q
- 此程式不一定會停下來
- 如果停下來的話，一定會停在滿足 Q 的地方
Total Correntness
- {P} C {Q} is true if and only if
- whenever C is executed in a state satisfying P the execution of C terminates
- after C terminates Q holds
