search
LoginSignup
1

More than 1 year has passed since last update.

Organization

Z3でテストケースを生成してみる

こんにちは。株式会社 日立製作所 研究開発グループの曾我 遼です。
この記事では、日立グループ OSS Advent Calendar 2020 の22日目として、Z3を用いてテストケースを生成する方法について紹介します。

Z3の説明

  • Z3とは、元々Microsoft Researchが開発していた、MITライセンスのOSSです(Githubページ)。
  • Z3は、SMT2形式で記述された論理式を受け取り、真とする値が存在するかどうか判定し、存在する場合は値を返します。
    • (例1)
      • (論理式) (and (= (+ x y) 10) (= (- x y) 6))
        • この論理式は、「$(x+y=10)$かつ$(x-y=6)$」を意味します。
      • (答え) 存在する。$(x, y) = (8, 2)$
    • (例2)
      • (論理式) (and (= x 1) (= x 2))
        • この論理式は、「$(x=1)$かつ$(x=2)$」を意味します。
      • (答え) 存在しない。
  • この記事では、Z3を使って、テストケースをどのように生成するのか紹介します。

テストケース作成の課題

  • テストケースとは、プログラムが期待通りに動くかどうかをテストするため、入力値とそれに対応した期待値を含むデータのことです。
  • 私が研究対象としている、COBOLプログラムを用いて説明します。

    • こちらのCOBOLプログラムは、$x=1$ のときに、$y$ に $1$ を加算するプログラムです。

      1 IF x = 1 THEN
      2   COMPUTE y = y + 1
      3 END-IF.
      
    • テストケースでは、「$x=1$ の時に、$y$ に $1$ 加算するかどうか」検証するため、入力値と期待値を準備します。

      • 入力値 : $x=1, y=0$
      • 期待値 : $y=1$
  • if文の数が多かったり、条件式が複雑だと、テストケースの作成がとても大変になります。

Z3を使ってテストケースの入力値を生成する

  • そこで、Z3を使って、テストケースを生成してみます。
  • この記事では、先ほどよりも難しい例に対して、入力値の生成例を示します。

    1 IF x = 1 THEN
    2   COMPUTE y = y + 1
    3 END-IF.
    4 IF x = 2 THEN
    5  COMPUTE y = y + 10
    6 END-IF.
    7 IF y = 100 THEN
    8   COMPUTE z = z + 1
    9 END-IF.
    
  • このプログラムには、変数へ値を代入する命令が、2,5,8行目にあります。

  • これらの命令をテストする入力値は、どうすれば生成できるのでしょうか。

欲張ったテスト方法:(2,5,8行目)を一気にテストする入力値はあるのか?

  • まず、欲張って、3つの命令を一気にテストできるのか確認してみましょう。
  • 人間の目で見ると、1行目と4行目のif文を両方真にするxの値は存在しないため、2,5,8行目を一気に検証する入力値がないことがすぐにわかります。
  • Z3で、同じことを証明できるでしょうか。

if文(1,4,7行目)に対応した論理式をSMT2形式で書いて、Z3を実行する

  • こちらに、1,4,7行目のif文に対応した論理式を示します。

    1. COBOLプログラムの変数を、SMT2形式で宣言。
    2. if文に対応した論理式の記述。1行目:(= x 1)、4行目:(= x 2)、7行目:(= (+ y 11) 100)
      • (7行目の論理式の補足) 7行目のif文の条件式へ、2,5行目を実行した結果を反映しています。
    3. 論理式を満たす値が存在するか判定。
    ; 変数の宣言
    (declare-const x Int)
    (declare-const y Int)
    (declare-const z Int)
    
    ; if文に対応した論理式
    (define-fun if_target () Bool (and (and (= x 1) (= x 2)) (= (+ y 11) 100))) 
    
    ; 論理式を満たす値が存在するか判定
    (assert if_target)
    (check-sat) 
    
  • Z3に論理式を入力・実行すると、unsat が出力されます。

  • これは、予想通り満たす値が存在しないことを意味します。

正しいテスト方法:(2,8行目)をテストする入力値はあるのか?

  • では、今度は、5行目の命令を除いた、2つの命令をテストできるか確認してみましょう。

if文(1,7行目)に対応した論理式をSMT2形式で書いて、Z3を実行する

  • こちらに、1,7行目のif文に対応した論理式を示します。

    1. COBOLプログラムの変数を、SMT2形式で宣言。
    2. if文に対応した論理式の記述。1行目:(= x 1)、7行目:(= (+ y 1) 100)
    3. 論理式を満たす値が存在するか判定。
    4. 論理式を満たす値を生成。
    ; 変数の宣言
    (declare-const x Int)
    (declare-const y Int)
    (declare-const z Int)
    
    ; if文に対応した論理式
    (define-fun if_target () Bool (and (= x 1) (= (+ y 1) 100)))
    
    ; 論理式を満たす値が存在するか判定
    (assert if_target)
    (check-sat)
    
    ; 論理式を満たす値を生成
    (get-model)
    
  • Z3に論理式を入力・実行すると、sat に続いて $x = 1, y = 99$ が出力されます。

  • これは、満たす値が存在して、2,8行目をテストする入力値を生成できたことを示します。

補足

  • Z3は、こちらのWebサイトにて、お試し実行できます。この記事で示した論理式を入力して、テストケースを生成してみてください。
  • 本記事に関連する研究として、国際会議(APSEC2020)で発表しました。
    • R. Soga, T. Yonemitsu, M. Inagaki, Y. Fujisaki, H. Sugou, H. Kanuka, “A Program Simplification Method for Generating Test Input Values Using Symbolic Execution,” in 2020 27th Asia-Pacific Software Engineering Conference(APSEC), 2020.

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
What you can do with signing up
1