Z3中一个if-else和while循环的验证条件

Question

我正在学习 Z3，想输入一些由霍尔逻辑规定的验证条件，并获得给定霍尔三元组的模型。

到目前为止我只能验证作业，这里有一个例子（只是为了检查我是否做对了）：

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-else 的 ite 命令，但它似乎不受支持。

希望你能帮助我。

Answer 1

这里有一些编码，ite的语法需要3个参数，第一个是条件，第二个是真实情况，第三个是错误情况（rise4fun link: http://rise4fun.com/Z3/qW3B ):

; original example for { x< 40  } x :=x+10 { x < 50}
(push)
(declare-const x Int)
(assert (< x 50))
(assert (< (+ x 10) 50 ))
(check-sat)
(get-model)
(pop)

; {0 ≤ x ≤ 15 }   if x < 15 then x := x + 1 else x := 0 endif   {0 ≤ x ≤ 15 }
(push)
(declare-const x Int)
(assert (and (>= x 0) (< x 15))) 
(assert (ite (< x 15) (and (>= (+ x 1) 0) (< (+ x 1) 15)) (and (= x 0) (>= x 0) (< x 15))))
(check-sat)
(get-model)
(pop)

; {x ≤ 10}   while x < 10 do x := x + 1 done   {¬x < 10 ∧ x ≤ 10}
(push)
(declare-const x Int)
(assert (and (<= x 10) (< x 10)))
(assert (and (not (< (+ x 1) 10)) (<= (+ x 1) 10)))
(check-sat)
(get-model)
(pop)

; the following are in strongest postcondition form, this typically makes more sense to me
(declare-const x_pre Int)
(declare-const x_post Int)

; { x< 40  } x :=x+10 { x < 50}
(push)
(assert (exists ((x_pre Int)) 
  (and (< x_pre 40) 
    (= x_post (+ x_pre 10))
    (< x_post 50 ))))
(check-sat)
(get-model)
(apply qe)
(pop)

; {0 ≤ x ≤ 15 }   if x < 15 then x := x + 1 else x := 0 endif   {0 ≤ x ≤ 15 }
(push)
(assert (exists ((x_pre Int)) 
  (and 
    (and (>= x_pre 0) (< x_pre 15)) 
    (ite (< x_pre 15) (= x_post (+ x_pre 1)) (= x_post 0)) 
    (and (>= x_post 0) (< x_post 15)))))
(check-sat)
(get-model)
(apply qe)
(pop)


; {x ≤ 10}   while x < 10 do x := x + 1 done   {¬x < 10 ∧ x ≤ 10}
(push)
(assert (exists ((x_pre Int)) 
  (and 
    (and 
      (<= x_pre 10) (< x_pre 10)) 
      (= x_post (+ x_pre 1))
      (and (not (< x_post 10)) (<= x_post 10)))))
(check-sat)
(get-model)
(apply qe)
(pop)

Z3中一个if-else和while循环的验证条件

Verification condition of an if-else and while loop in Z3

z3

hoare-logic