Условие проверки цикла if-else и while в Z3

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 }

Или Хотя циклы (частичная корректность)

{x ≤ 10} while x < 10 do x := x + 1 done {¬x < 10 ∧ x ≤ 10}

Я попытался с помощью команды ite для if-else, но, похоже, не поддерживается.

Надеюсь, вы можете мне помочь.

Answer 1

Here're некоторые кодировки, синтаксис для 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)