Z3不変チェック

Question

不変量と1つまたは複数の操作の効果が与えられた場合、操作の実行後に不変条件がまだ成立しているかどうかを確認します。

これを達成するためのアイデアはありますか？ UNSAT返します（チェック・土）の場合、私は

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

に似た何かを考えていたZ3を使用して

はその後、私は、システムの状態は、操作後に有効であると結論付けています。

私は明らかにいつも定理はUNSAT作る

(assert invariant) 
(assert (not invariant)) 

ので、上記を行うことはできません。

しかし、私が実行すると（assert（不変でない））、操作によって変更されないシステムの部分が有効になるように、初期状態が有効であることを主張する必要があります。

Answer 1

私はあなたの操作が何らかの種類の状態（ローカル変数、プログラムヒープなど）を変更したと仮定しているため、あなたのインバリアントはのの状態になるはずです。

小さな例として、ローカル変数を使用してこの仮説必須プログラムを考慮する：

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 

変異ローカル変数は静的単一代入形式で表現される場合、次のように符号化することができた：

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