Z3中if-else和while循环的验证条件答案

【问题标题】：Verification condition of an if-else and while loop in Z3Z3中if-else和while循环的验证条件
【发布时间】：2015-05-07 23:15:15
【问题描述】：

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

到目前为止，我只能验证分配，这是一个示例（只是为了检查我是否做对了）：

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

希望你能帮我解决这个问题。

【问题讨论】：

标签： z3 hoare-logic

【解决方案1】：

这里有一些编码，ite的语法需要3个参数，第一个是条件，第二个是真，第三个是假（rise4fun链接：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)

【讨论】：