Academia Sinica IIS Intern [Learning] - Program Verification

# Academia Sinica IIS Intern [Learing] - Program Verification > 形式化驗證的學習與筆記 [name=dd]  ## 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)