Z3 invariant check

Question

I want a way to, given an invariant and one or more operation's effects, check if, after the operation's execution, the invariant still holds.

Any ideas on how to accomplish this?

Using Z3 I was thinking of doing something similar to

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)

(define-fun invariant () Bool
  (= a b c d 2)
)

(assert invariant)
(assert (= a 1)) ;operation1
(assert (= b 2)) ;operation2
(assert (not invariant))
(check-sat)

If (check-sat) returns unsat then I conclude that the system's state is valid after the operations.

I obviously can't do the above since

(assert invariant)
(assert (not invariant))

always make the theorem unsat.

But I need to assert that the initial state is valid so that the parts of the system that aren't changed by the operations are valid when I run (assert (not invariant)).

This presentation by Cesare Tinelli might be relevant for you. — Patrick Trentin
I realize (assert (= a 1)) isn't an assignment. I was just trying to model the states of the system as an example. I don't know if I made myself clear enough. The presentation seems relevant, it is taking me however sometime to interpret it's contents. Thank you for the suggestion. — user2009400

Malte Schwerhoff Malte Schwerhoff · Accepted Answer · 2016-06-23T06:31:47

I assume that your operations mutate some kind of state (local variables, a program heap, ...), and your invariant should therefore be a function of the state.

As a small example, consider this hypothetical imperative program with local variables:

var start: Int := 0
var end: Int := 0
var arr: Array[Int] := new Array(10) // Array of ints, size 10
fill(arr, 0) // Fill the array with zeros

def invariant() =
     (0 < start <= end)
  && forall i in [start, end - 1) :: arr(i) < arr(i + 1) // Sorted

assert invariant() // holds
end := end + 1
assert invariant() // holds
end := end + 1
assert invariant() // fails
arr(start + 1) := arr(start + 1) + 1
assert invariant() // holds

It could be encoded as follows, where the mutated local variables are represented in static single assignment form:

(define-fun invariant ((start Int) (end Int) (arr (Array Int Int))) Bool
  (and
    (<= 0 start)
    (<= start end)
    (forall ((i Int))
      (implies
        (and (<= start i) (< i (- end 1)))
        (< (select arr i) (select arr (+ i 1)))))))

(declare-const start0 Int)
(declare-const end0 Int)
(declare-const arr0 (Array Int Int))

(assert (= start0 0))
(assert (= end0 0))
(assert (= arr0 ((as const (Array Int Int)) 0)))

(push)
  (assert (not (invariant start0 end0 arr0)))
  (check-sat) ;; UNSAT --> Invariant holds
(pop)

;; Operation: end := end + 1

(declare-const end1 Int)
(assert (= end1 (+ end0 1)))

(push)
  (assert (not (invariant start0 end1 arr0)))
  (check-sat) ; UNSAT --> Invariant still holds
(pop)

;; Operation: end := end + 1

(declare-const end2 Int)
(assert (= end2 (+ end1 1)))

(push)
  (assert (not (invariant start0 end2 arr0)))
  (check-sat) ; SAT --> Invariant has been broken!
(pop)

;; Operation: arr[start + 1] := arr[start + 1] + 1

(declare-const arr1 (Array Int Int))
(assert (= arr1 (store arr0 (+ start0 1) (+ (select arr0 (+ start0 1)) 1))))

(push)  
  (assert (not (invariant start0 end2 arr1)))
  (check-sat) ; UNSAT --> Invariant has been restored
(pop)

Z3 invariant check

1 Answers