Academia Sinica IIS Intern [Learing] - Program Verification

• Hoare Logic
• Z3

D

Program Verification

Section 1 - A framework 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 {C} else {C} | 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
• 此程式一定會停下來，且 ψ 會一定會符合

Program variables and Logical variables

Program variables

• free variables in the pre- and post-conditions of a Hoare triple (|φ|) P (|ψ|) are program variables

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

y = 1;
while (x != 0){
    y = y * x;
    x = x - 1;
}

• (|x = x0 Λ x ≥ 0|) Fac1 (|y = x0!|)
  • 在一開始就先將 x 另外存在其餘的變數 (x₀)，而 x₀ 並沒有出現在程式裡，所以數值不會被更改，因此 x₀ 左右兩邊都相等，根據 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{(|\phi |)C_0(|\eta |)(|\eta |)C_1(|\psi |)}{(|\phi |)C_0;C_1(|\psi |)}$

Assignment

$\frac{}{(|\psi [E/x]|)x=E(|\psi |)}$

If

$\frac{(|\phi \wedge B|)C_0(|\psi |)(|\phi \wedge \neg B|)C_1(|\psi |)}{(|\phi |)ifB\{C_0\}else\{C_1\}(|\psi |)}$

While

$\frac{(|\psi \wedge B|)C(|\psi |)}{(|\psi |)whileB\{C\}(|\psi \wedge \neg B|)}$

Implied

$\frac{{⊢}_{AR}{\phi }^{\prime }\Rightarrow \phi (|\phi |)C(|\psi |){⊢}_{AR}\psi \Rightarrow {\psi }^{\prime }}{(|{\phi }^{\prime }|)C(|{\psi }^{\prime }|)}$

Proof Tableaux

呃呃呃 我真的懶得寫了 嗚嗚嗚
有空再說吧(那應該就是不會寫了哈哈
反正這邊的概念就是將 postcondiction，根據每個條件(可以看 Proof Rules)，推出 precondiction

Section 3 - Proof calculus for total correctness

Section 4 - Introduction to Z3

SMT and SAT

• SAT
  • Boolean Satisfiability Theories
  • 只能解決 Boolean Satisfiability Problem，也就是給定一個 Boolean 公式，判斷是否存在一組變量的真值賦值使得整個公式為真
  • SAT solvers have been used in hardware verification
  • SAT solvers 很難驗證程式，因為他沒辦法提供數學運算的處理，SAT solvers 只能幫助解決簡單問題
• SMT
  • Satisfiability Modulo Theories
  • many SMT solvers are based on SAT solvers
  • SMT solvers are SAT solvers extended with various theories (theories of linear arithmetic, uninterpreted functions…)
  • SMT solveres can varitify program

Z3

• using Z3 in Python

from z3 import *

s = Solver()

print(s.check())
print(s.model())

Reference

• 形式化驗證入門