テストケース自動生成器をつくる

8 min read読了の目安(約7600字

はじめに

プログラムから自動的にテストケースを生成するテストケース生成器を作ってみます.

プログラミング言語は Scheme, 処理系は Gauche を使います。

プログラムの構文

プログラムの構文は次のようにします。S式です。

(prog 変数リスト 事前条件 文)

変数は整数型だけとします。

文は5種類用意します:

  • skip
  • (set! 変数 式)
  • (if 条件 文 文)
  • (while 条件 文)
  • (block 文 ...)

式は前置記法で、次の演算子を用意します:

  • and
  • or
  • not
  • =
  • >
  • <
  • >=
  • <=
  • +
  • -
  • div

しくみ

基本的な考え方: if 文の条件に着目する

プログラムからテストケースを作るときは,if 文に着目して,その条件が成り立つ場合と成り立たない場合をそれぞれテストケースとします.

この条件を,プログラムの入口の方に向かって変換していって,プログラムの先頭で成り立つべき条件が得られれば,それがテストケースになります.

あとは SMT-solver Z3 に条件を投げて,変数への具体的な値の割り当てを作ってもらいます.

複数の if 文があるとき

複数の if 文があるときは,それぞれ2つに分けてもいいですが,より徹底的に調べたい場合は,すべての組み合わせを考えます.たとえば

(block (if a X Y) (if b U V))

とあったら,a, (not a), b, (not b) の4通りではなく,パスの組み合わせで考えて,(and a b), (and (not a) b), (and a (not b)), (and (not a) (not b)) の4通りを考えます.

ループはどうする?

ループがあると条件をプログラムの入り口に向かって変換することができません.そこで,ここではテストですから開き直ってループの実行回数に上限を設けてしまうことにします.ループが1回も回らない場合,1回だけ回る場合,2回だけ回る場合と列挙して,それぞれテストケースになるようにします.

かんたんのため,ループがネストしてる場合は考えないことにします.

プログラム

プログラムの構文にしたがって再帰的に処理します.ループの最大実行回数を n, 着目しているプログラムの位置でのテストケースの条件のリストを ps とします.

空文 skip

文が skip の場合は何もすることがありません.

代入文 (set! var expr)

字句代入を使うと条件を代入実行前の条件に変換できます.

条件文 (if test stmt1 stmt2)

if 文 の場合は,条件 test が成り立つ場合と成り立たない場合に分けます.先に ps を stmt1, stmt2 実行前の条件リストに変換します.これをそれぞれ ps1, ps2 としましょう.もし ps1 が空の場合は,テストケースとして test を加えます.そうでなければ ps1 の各要素 p について (and test p) を作ります.条件が成り立たない場合も同じです.

ループ (while test stmt)

ループは展開します.難しそうですけど,次のように考えればかんたんです.
もし展開の回数 n が 0 だったら何もしません.そうでない場合は

(while B S) = (if B (block S (while B S)) skip)

ですから,これを使って再帰的に処理すれば OK です.

条件の計算

以上の考察をまとめるとこんな感じ.

(define (wp n stmt ps)
  (match stmt
    ('skip ps)
    (('set! var expr)
     (map (lambda (p) (subst var expr p)) ps))
    (('if test stmt1 stmt2)
     (let ((ps1 (wp n stmt1 ps))
           (ps2 (wp n stmt2 ps)))
       (append 
        (if (null? ps1)
            (list test)
            (map (lambda (p) `(and ,test ,p)) ps1))
        (if (null? ps2)
            (list `(not ,test))
            (map (lambda (p) `(and (not ,test) ,p)) ps2)))))
    (('while test stmt)
     (if (= n 0)
         ps
         (wp (- n 1)
             `(if ,test (block ,stmt (while ,test ,stmt)) skip)
             ps)))
    (('block . stmt-list)
     (fold-right
       (lambda (stmt ps) (wp n stmt ps))
       ps stmt-list))
    (_
     (error "unknown statement" stmt))))

テストしてみます.

まず if 文1個:

(wp 0 '(if b skip skip) '())
=> (b (not b))

ps が空でない場合は,テストそのものの代わりに and がつく:

(wp 0 '(if b skip skip) '(a))
=> ((and b a) (and (not b) a))

if 文がネストしている場合:

(wp 0 '(if a (if b skip skip) skip) '())
=> ((and a b) (and a (not b)) (not a))

横並びの if 文では条件が組み合わせになる:

(wp 0 '(block (if a skip skip) (if b skip skip)) '())
=> ((and a b) (and a (not b)) (and (not a) b) (and (not a) (not b)))

条件の前に文がある場合はさかのぼって変換:

(wp 0 '(block (set! x (- x 1)) (if (> x 0) skip skip)) '())
=> ((> (- x 1) 0) (not (> (- x 1) 0)))

ループの場合 (n=3):

(wp 3 '(while (> x 0) (set! x (- x 1))) '())
=> ((and (> x 0) (and (> (- x 1) 0) (> (- (- x 1) 1) 0)))
    (and (> x 0) (and (> (- x 1) 0) (not (> (- (- x 1) 1) 0))))
    (and (> x 0) (not (> (- x 1) 0)))
    (not (> x 0)))

式を整理してみると

((> x 2)
 (and (> x 1) (<= x 2))
 (and (> x 0) (<= x 1))
 (<= x 0))

となって,ループの実行回数が3回,2回,1回,0回の場合に対応することがわかります.

字句代入

(define (subst x e p)
  (cond ((symbol? p)
         (if (eq? x p) e p))
        ((pair? p)
         (cons (subst x e (car p))
               (subst x e (cdr p))))
        (else p)))

条件式を Z3 のモデルに変換

(define (gen-model vars assertion)
  (let ((port (open-output-file "model.z3")))
    (for-each
      (lambda (var)
        (format port "(declare-const ~A Int)\n" var))
      vars)
    (format port "(assert ~A)\n" assertion)
    (format port "(check-sat)\n(get-model)\n")
    (close-port port)))

main

  1. まず wp を使ってテストケースの条件リストを作ります.
  2. それぞれ Z3 のモデルに変換してから Z3 に投げます.

各条件には事前条件を and しておきます.成立しない条件もあります.

(define (tcg n prog)
  (match prog
    (('prog vars pre stmt)
     (let ((ps (map (lambda (p) `(and ,pre ,p))
                    (wp n stmt '()))))
       (for-each
         (lambda (p)
           (gen-model vars p)
           (sys-system "z3 -smt2 model.z3"))
         ps)))))

プログラムは以上です.

使ってみる

if 文1個

if 文が1個あるだけです.事前条件は true ですけど,書き方がわからないのでこんなふうにしました.

(tcg
 0
 '(prog (x)
        (= 0 0)
        (if (>= x 0)
            skip
            skip)))

実行するとテストケースが2つ得られます.

sat
(model 
  (define-fun x () Int
    0)
)
sat
(model 
  (define-fun x () Int
    (- 1))
)

if 文ネスト

(tcg
 0
 '(prog (x)
        (= 0 0)
        (if (>= x 0)
            (if (= x 0)
                skip
                skip)
            skip)))

テストケースが3つ得られます.

sat
(model 
  (define-fun x () Int
    0)
)
sat
(model 
  (define-fun x () Int
    1)
)
sat
(model 
  (define-fun x () Int
    (- 1))
)

if 文2個

横並びの if 文も組み合わせになります.

(tcg
 0
 '(prog (x y)
        (= 0 0)
        (block
         (if (> x 0)
             skip
             skip)
         (if (> y 0)
             skip
             skip))))

生成されたテストケースを見ると,確かに組み合わせになってます.

sat
(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    1)
)
sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    1)
)
sat
(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    0)
)
sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    0)
)

単純なループ

変数をデクリメントするだけのループです.展開の上限を3にしてみました.

(tcg
 3
 '(prog (x s)
        (= 0 0)
        (while (> x 0)
          (set! x (- x 1)))))

0, 1, 2, 3 回まわることになるので,それぞれ対応するテストケースが出てきます.

sat
(model 
  (define-fun x () Int
    3)
)
sat
(model 
  (define-fun x () Int
    2)
)
sat
(model 
  (define-fun x () Int
    1)
)
sat
(model 
  (define-fun x () Int
    0)
)

ちょっと込み入ったループ

二分探索のまねごとをするループです.

(tcg
 4
 '(prog (x a b m)
        (and (<= 0 a) (<= a m) (<= m b))
        (while (< a b)
          (block
           (set! x (div (+ a b) 2))
           (if (= x m)
               (set! b a)
               (if (< x m)
                   (set! a (+ x 1))
                   (set! b (- x 1))))))))

テストケースは 46 個出てきました.Z3 出力のままだと見にくいので,(a b m) のリストにするとこうなります.

((0 1 0) (0 3 2) (0 7 6) (0 15 14) (0 15 15) (0 23 21) (0 7 7)
 (0 27 22) (0 19 16) (0 27 21) (0 11 9) (0 3 3) (0 13 8) (0 25 17)
 (0 17 12) (0 25 16) (0 9 6) (0 29 16) (0 21 12) (0 29 15) (0 13 7)
 (0 5 3) (0 1 1) (0 4 0) (38 46 40) (0 16 6) (0 16 7) (0 24 9) 
 (38 46 41) (0 28 8) (1236 1256 1242) (0 28 7) (0 12 3) (0 4 1) 
 (0 10 0) (38 56 40) (38 56 41) (0 26 3) (0 10 1) (0 22 0) (0 22 1)
 (38 68 38) (38 52 38) (38 44 38) (0 3 0) (0 0 0))

なんだかよくわからないので,上のプログラムと同じ Scheme の関数を書いてみます.

(define (f a b m)
  (let loop ((a a) (b b))
    (if (< a b)
        (let ((x (div (+ a b) 2)))
          (cond ((= x m)
                 (loop a a))
                ((< x m)
                 (display "1")
                 (loop (+ x 1) b))
                (else
                 (display "2")
                 (loop a (- x 1)))))
        (newline))))

ループの内の if 文がどちらに行くかで 1, 2 を表示させます.
これを生成されたテストケースに適用してみると...

1
11
111
1111
1112
111
112
1121
1122
112
11
12
121
1211
1212
121
122
1221
1222
122
12
1
2
21
211
2111
2112
211
212
2121
2122
212
21
22
221
2211
2212
221
222
2221
2222
222
22
2

各ループの実行回数ごとに,それぞれの実行で分岐のどちらにいくかの組み合わせがすべて生成されていることが見て取れます.

おわりに

条件の and/or でもっと細かくテストケースを分けたり,ループのネストに対応するとおもしろいかもしれません.