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

Question

I'm learning Z3 and want to input some verification condition as stated by the Hoare logic and obtain a model of the given Hoare triples.

So far I have only been able to verify assignments, here is an example (just to check if I'm doing it right):

Given: { x< 40 } x :=x+10 { x < 50}

(declare-const x Int)
(assert (< x 50))
(assert (< (+ x 10) 50 ))
(check-sat)

But I don't know how to verify If-Else like:

{0 ≤ x ≤ 15 } if x < 15 then x := x + 1 else x := 0 endif {0 ≤ x ≤ 15 }

Or While loops (partial correctness)

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

I tried with the ite command for the if-else but it seems to be unsupported.

Hope you can help me with this.

Taylor T. Johnson · Accepted Answer · 2015-05-08T06:00:39.467

Here're some encodings, the syntax for ite requires 3 parameters, the first of which is the conditional, the second is the true case, and the third is the false case (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)

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

1 Answers1