2
我正在學習Z3並希望輸入Hoare邏輯所述的一些驗證條件,並獲得給定Hoare三元組的模型。Z3中if-else和while循環的驗證條件
到目前爲止,我只能夠驗證任務,這裏有一個例子(只是爲了檢查,如果我這樣做是正確的):
Given: { x< 40 } x :=x+10 { x < 50}
(declare-const x Int)
(assert (< x 50))
(assert (< (+ x 10) 50))
(check-sat)
但我不知道如何驗證的if-else這樣的:
{0 ≤ x ≤ 15 } if x < 15 then x := x + 1 else x := 0 endif {0 ≤ x ≤ 15 }
或者while(部分正確性)
{x ≤ 10} while x < 10 do x := x + 1 done {¬x < 10 ∧ x ≤ 10}
我試着用if命令的ite命令,但它似乎不受支持。
希望你能幫助我。