---
# System prepended metadata

title: 'Academia Sinica IIS Intern [Learning] - Program Verification'
tags: [中研院 IIS, internship]

---

# Academia Sinica IIS Intern [Learing] - Program Verification
> 形式化驗證的學習與筆記 [name=dd]
<!-- ## 前言
### 動機
### 驗證技術的分類
### Why not Model Checking ? -->
## Section 1 - A framework for software verification
- framework
    - informal description R of requirements -> formula φ~R~
### A core programming language
- Integer expressions
    - `E ::= n | x | (-E) | (E + E) | (E - E) | (E * E)`
- Boolean expressions
    - `B ::= false | true | (!B) | (B && B) | (B || B) | (E < E)`
- Commands
    - `C ::= x = E | C ; C | if B {C0} else {C1} | while B {C}`
### Hoare triples
-  `(|φ|) P (|ψ|)`
    - `|φ|` : Precondition
    - `P` : 程式碼
    - `|ψ|` : Postcondition
### Partial and total correctness
total correctness 的限制基礎是基於 partial correctness 之上，所以證明 total correctness 會比證明 partial correctness 還要困難，因此我們將專注於證明 partial correctness
#### Partial Correctness
- `(|φ|) P (|ψ|)` is true if
    - whenever `P` is executed in a state satisfying `φ`
    - and if the execution of `P` terminates
    - then the state in which `P`'s execution terminates satisfies `ψ`
> 此程式不一定會停下來，如果停下來的話，一定會停在符合 `ψ` 狀態的地方
#### Total Correctness
- `(|φ|) P (|ψ|)` is true if and only if
    - whenever `P` is executed in a state satisfying `φ` the execution of `P` terminates
    - after `P` terminates `ψ` holds
> 此程式一定會停下來，且 `ψ` 會一定會符合
#### 例子
```
(|⊤|) while true x = x (|⊥|)
```
- partial correctness：成立，因為 P 不會終止，所以 `ψ` 為 true 或 false 都沒差
- total correctness：不成立，因為 P 不會終止，不符合定義 
### Program variables and logical variables
#### Program variables
- free variables in the pre- and post-conditions of a Hoare triple `(|φ|) P (|ψ|)` are program variables
```cpp=
y = 1;
while (x != 0){
    y = y * x;
    x = x - 1;
}
```
```
(|x ≥ 0|) Fac1 (|y = x!|)
```
- 左邊的 x，為執行 Fac1 前，符合 precondition 的 x
- 右邊的 x，為執行 Fac1 後，程式會停下來且符合 postcondition 的 x
- 左右兩邊的 x 不相同，因此根據 Hoare triple，Fac1 is incorrect
#### Logical Variables
- one way to specify Fac1 is to introduce logical varialbes, a logical variable occurs only in logic formula but not programs
```cpp=
y = 1;
while (x != 0){
    y = y * x;
    x = x - 1;
}
```
```
(|x = x0 Λ x ≥ 0|) Fac1 (|y = x0!|)
```
- 在一開始就先將 x 另外存在其餘的變數 (x~0~)，而 x~0~ 並沒有出現在程式裡，所以數值不會被更改，因此 x~0~ 左右兩邊都相等，根據 Hoare triple，Fact1 is correct

## Section 2 - Proof calculus for partial correctness
we can use **proof rules** and **proof tableaux** to make a **proof tree**, than prove the programs

### Proof Rules
#### Composition

$\frac{(|φ|)C_{0}(|η|)\space\space(|η|)C_{1}(|ψ|)}{(|φ|)C_{0};C_{1}(|ψ|)}$

#### Assignment
$\frac{}{(|ψ[E/x]|)x = E(|ψ|)}$
#### If

$\frac{(|φ ∧ B|)C_{0}(|ψ|)\space\space(|φ ∧ ¬B|)C_{1}(|ψ|)}{(|φ|)\space if\space  B\space \{ {C_{0}}\}\space else \space\{ {C_{1}}\}(|ψ|)}$

#### While
$\frac{(|ψ ∧ B|)C(|ψ|)}{(|ψ|)while\space B\space \{ C \} \space(|ψ ∧ ¬B|)}$
- invariant 不變量、不變式
    - 始終保持成立的條件
    - 在程式執行前、中、後，都為 true
#### Implied
$\frac{\vdash _{AR}\space φ' ⇒ φ \space (|φ|)C(|ψ|) \vdash _{AR}\space ψ ⇒ ψ'}{(|φ'|)C(|ψ'|)}$

### Proof Tableaux
這邊的概念就是將 postcondiction，根據每個條件(可以看 Proof Rules)，推出 precondiction
## Section 3 - Proof calculus for total correctness
在規則中，while 是唯一非終止語句，因此，除了部分 while 規則以外，total correctness 的證明規則和 partical correctness 的證明規則相同
## Section 4 - Introduction to Z3
### SMT and SAT
- SAT（Boolean **Sat**isfiability Theories）
    - 只能解決 Boolean Satisfiability Problem，給定一個 Boolean 公式，判斷是否存在一組變量的真值、賦值，使得整個公式為真
    - SAT solvers 被使用在硬體驗證（digital circuits），很難驗證程式，因為它沒辦法提供數學運算的處理，只能幫助解決簡單問題
- SMT（Satisfiability Modulo Theories）
    - many SMT solvers are based on SAT solvers，除了 Boolean 公式，還可以加入數學或程式相關的 theories (linear arithmetic, uninterpreted functions...)
    - SMT solvers 可以驗證程式
### Z3
SMT solver
- using Z3 in Python
```python=
from z3 import *

s = Solver()

print(s.check())
print(s.model())
```
## More
- [Hoare Logic](/1ZlKSNijQCyJyf-gnCGjKQ)
- [Z3](/YIDiWETPRPG4EBoV4uTmjw)
## Reference
- [王柏堯老師的簡報](https://homepage.iis.sinica.edu.tw/~bywang/courses/comp-logic/)
- [形式化驗證入門](https://hackmd.io/@umBhzVYqQXOkdc_91WUbrw/HyJXQBk6W?type=view)