Z3-Invariant-Check

Question

Ich möchte einen Weg, eine invariante und eine oder mehrere Operation Auswirkungen, überprüfen Sie, ob nach der Ausführung der Operation die Invariante immer noch gilt.

Irgendwelche Ideen, wie dies zu erreichen ist?

Z3 Verwendung Ich dachte an etwas Ähnliches tun zu

(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) 

Wenn (Check-sat) gibt unsat dann schließe ich, dass das staatliche System nach den Operationen gültig ist.

Ich kann natürlich nicht die oben tun, da

(assert invariant) 
(assert (not invariant)) 

immer den Satz unsat machen.

Aber ich muss feststellen, dass der Anfangszustand gültig ist, so dass die Teile des Systems, die nicht von den Operationen geändert werden, gültig sind, wenn ich (assert (nicht invariant)) ausführen.

Answer 1

Ich gehe davon aus, dass Ihre Operationen eine Art von Zustand mutieren (lokale Variablen, ein Programm-Heap, ...), und Ihre Invariante sollte daher eine Funktion von der Staat sein.

Als kleines Beispiel dieses hypothetischen Imperativ Programm mit lokalen Variablen:

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 

Es könnte wie folgt codiert werden, wobei die mutierten lokalen Variablen in statischer Einzelzuordnung Form dargestellt werden:

(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)