3

我正在学习 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 命令，但它似乎不受支持。

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

4

1 回答 1

4

这里有一些编码，语法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)
于 2015-05-08T03:01:54.297 回答