# Academia Sinica IIS Intern [Learning] - Hoare Logic
> Hoare Logic 補充 [name=D]
## Hoare triples
Hoare triple 透過 state 來定義 pre-condition \(P) 和 post-condition (Q)，來確保程式 \(C) 的正確性
- state 的定義
- 程式執行時所有變數的當前值
- {P} C {Q}
- P : 斷言(執行前要滿足的狀態)
- Q : 斷言(執行後要滿足的狀態)
- C : 命令(要執行的程式)
## Partial and Total Correctness
### Partial Correctness
- 程式不一定會終止，如果終止了，那麼它的結果一定滿足 Q
- partial correctness 只保證結果正確，但不保證程式一定會結束

:::info
{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
:::

### Total Correntness
- 程式一定會終止，而且執行後的結果滿足 Q

:::info
- {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
:::
## Reference
- [Hoare Logic](https://www.cl.cam.ac.uk/archive/mjcg/HoareLogic/Lectures/AllLectures.pdf)