社団法人 電子情報通信学会
THE INSTITUTE OF ELECTRONICS,INFORMATION AND COMMUNICATION ENGINEERS

信学技報
TECHNICAL REPORT OF IEICE.

SMT ソルバーと PDG 作成ツールを用いた
Java のテストケース自動導出手法の提案
佐々木幸広†

小林 和貴†

岡野 浩三†

楠本真二†† 大阪大学大学院情報科学研究科〒 565-0871 大阪府吹田市山田丘 1-5
E-mail: †y-sasaki@ics.es.osaka-u.ac.jp, †{k-kobays,okano,kusumoto}@ist.osaka-u.ac.jp
あらましDesign by Contract に基づく表明の生成手法には静的生成手法と動的生成手法が存在する．動的生成手法

では，テストケースを用いて引数やフィールド変数の値を変えながら対象メソッドを解析し，データを取得するため，比較的少ないコストで表明を生成できる．一方で，テストケースがどれだけの実行範囲をカバーしているかというテストケースの質が生成される表明の質に影響を与える．この問題に対し，インバリアントカバレッジという指標が存在する．本研究では対象メソッドの PDG からインバリアントカバレッジを満たす可能性のある実行パスを列挙し SMTソルバを用いてそのパスの実行可能性と具体的な引数値の導出を行う方法を提案する．また，複数の例題に適用し有効であることを確認した．
キーワード

SMT ソルバ, PDG, Daikon, テストケース, Java

Automatic derivation of test cases for Java using an SMT solver
and a PDG generator
Yukihiro SASAKI† , Kazuki KOBAYASHI† , Kozo OKANO† , and Shinji KUSUMOTO†† Osaka University
E-mail: †y-sasaki@ics.es.osaka-u.ac.jp, †{k-kobays,okano,kusumoto}@ist.osaka-u.ac.jp
Abstract Assertions and Design by Contract play important roles for program understanding and program verification. In order to generate assertions, there are two kinds of methods, static analysis and dynamic analysis.
Dynamic approach needs less CPU times, however suﬀers the test case depending problem in which the quality ofassertions depends on the quality of test cases. Invariant coverage is one of indicator to specify the quality of test
cases. In other words, the coverage of test cases aﬀects the quality of generated assertions. The proposed method
uses PDG of a target method to generate a candiate path set and uses an SMT solver to decide whether a candidate
path is executable or not, as well as a concrete set of real parameters. We have implemented a tool and evaluatedthe usefulness of the proposed method through several programs.
Key words SMT solver, PDG, Daikon, test case, Java

1. は じ め に用いてプログラムを検証できる．これによりプログラムの保守性や信頼性が向上する．しかし，プログラムのソースコード量オブジェクト指向ソフトウェアの設計における Design byの増大により，人手で表明をソースコードに記述するのは困難

Contract(DbC) [1] はプログラムにおける仕様をソースコードとなる．これを解決するために，表明を自動で導出するツール中に記述することにより，ソフトウェア開発における誤りの箇として Daikon [4, 5] がある．しかし，テストケースがどれだけ所を明確にする手法である．これにより，仕様理解の補助やプの実行範囲をカバーしているかというテストケースの質が生成ログラムの妥当性を確認できる．Java 言語においてはプログラされる表明の質に影響を与える [6]．そこで，著者らが所属すムのソースコード中に事前条件・事後条件・不変条件などを表る研究グループでは，表明導出に利用するために有効なテスト明という形で記述し，静的解析ツール ESC/Java2 [2, 3] などをケースを自動で生成する手法を研究している．

—1—

本報告の提案手法では，対象プログラムのメソッドに対して，プログラム依存グラフ (PDG) [7] からインバリアントカバ
レッジ [8, 9] に影響を及ぼす実行パスを抽出する．そしてインバリアントカバレッジを満たすパスを SMT ソルバ [10, 11] の文法 SMT-lib2.0 Standard [12] 文法に準拠した制約式に変換し，SMT ソルバの解を用いてテストケースを導出する手法で

01: int example(int x, int y) {02: int ret=0;
03: if (x > 0) {04: x=x+2*3;
05: ret=y;
06: }
07:
08:
return ret;
09: }

ある．
また，本稿において提案した手法を実装した．ツール全体で

図 1 メソッド example のソースコードの出力の妥当性を検証するため，Java プログラムのソースコー

int example(int,int)

ドに対してツールを適用する実験を行った．その結果，いくつ

int x <1>

int ret = 0; <2>かのメソッドに関して本稿で示す既存手法 [13] の課題点を解消
x>0 <3>する結果が出力された．
以降，2 章で研究の背景について述べ，3 章で提案手法について述べ，4 章で評価について述べ，5 章でまとめる．

2. 準

備

x=x+2*3;<4>

データ依存

int y <1>

ret=y;<5>

制御依存研究の背景となる諸技術と関連研究について簡単に触れる．

2. 1 表return ret; <8>

明Java プログラムにおいては，ソースコード中に表明と呼ば図 2 メソッド example の PDGれる記述を行うことにより，DbC における契約を記述できる．
この表明により，ESC/Java2 などの静的解析器を用いて，プ

2. 3 テストケース依存問題

ログラムの妥当性を検証することで，開発者の意図しない不具

動的生成手法により表明を自動生成するとき，生成される表合の混入を防止できる．

明の精度は入力であるテストケースの品質に依存する．これを2. 2 表明の自動導出手法

テストケース依存問題と呼ぶ．動的生成手法で用いるテスト

ソースコードサイズの増加に伴い，人手による表明記述は困

ケースは対象メソッドの引数生成部とその引数が満たすべき条難となる．そこで，表明の自動生成手法が注目されている．表

件，対象メソッド呼び出しの 3 つからなる手続きであるが，こ明の生成の自動化手法に，静的手法と動的手法の 2 種類があの引数の条件が十分でない場合，実行パスの網羅性が保証される [14]．

ず，得られる実行データが少なくなる．このとき，限定的ある

2. 2. 1 表明の静的自動導出手法
表明の静的自動導出手法はソースコードの状態を表すモデル

いは誤った表明が生成されてしまう場合がある．

2. 4 インバリアントカバレッジ

を生成し，実行し得る全ての状態とそのときの実行条件を求め

インバリアントカバレッジは，表明の動的生成ツールに用いることで，表明を生成する．そのため，精度の高い表明を自動るテストケースの品質測定を目的として提案されたカバレッジ生成できる．Houdini [15] は静的解析器 ESC/Java2 を繰り返である．このカバレッジに基づいてテストケースを生成するこし適用することにより，表明を生成する．しかし，一般的にモとで，テストケース依存問題を改善できる．インバリアントカ

デルの状態数に対するスケーラビリティが課題である．

バレッジは一般的な表明の生成に必要な全実行パスに対して，2. 2. 2 表明の動的自動導出手法
表明の動的自動導出手法は対象ソースコードとテストケーステストケースが実際に実行する実行パスの割合を示す [8, 18]．

2. 5 プログラム依存グラフ

を入力とし，テストケースを用いて対象ソースコードを実行し，プログラム依存グラフ (PDG) とは，プログラム中の命令を得られたデータから表明を生成する．ここでテストケースとは，ノード，ノード間の依存関係を有向辺で表したグラフである [7]．

対象メソッドの引数生成部とその引数が満たすべき条件，対象主な依存関係には制御依存とデータ依存がある．制御依存辺はメソッド呼び出しの 3 つからなる手続きである．テストケース

次に実行しうるノード間に構築され，データ依存辺はデータ依の品質が低い場合，生成される表明の精度が低下する問題が指存があるノード間に構築される．図 1 で示すメソッドに対する摘されているが，一般的に比較的少ない時間とメモリで表明をPDG を図 2 に示す．

生成できる．そのため，動的手法は表明の自動生成に用いられ

2. 6 SMT ソルバることが多く，その代表的ツールとして Daikon がある．このSMT [10](Satifiablity Modulo Theories) は特定の分野の数ツールを用いることで，手作業で表明を記述するより表明生成学的な体系を表す理論である．例えば，算術の理論，集合の理に必要な時間的，人的コストを軽減できる．また，実際にプロ論などがある [11]．幾つかの SMT ソルバでは一階述語論理のグラムを実行した結果を用いるため，プログラマがソースコー充足可能性判定問題を解くことができる．なお，充足の可否だ

ド記述時には気づかなかった表明を生成することもできる．こけでなく，充足する場合の変数への割り当て方の情報も含む．

れはプログラムの保守，デバッグに有効である．

—2—

2. 7 Z3
Z3 [16] は，Microsoft 社が開発した SMT ソルバである．自り，既存研究のテストケース生成手法を改善できる．

3. 1 提案手法概要

社で開発するプログラム解析，テスト，検証など様々なツール

入力:Java の１メソッド

内で Z3 を利用している [11]．Z3 は本研究で用いる SMT ソル

出力:テストケース

バであり，線形の実数や整数の算術や配列，レコードの表現な（ 1 ） 対象メソッドの PDG を生成する．

ど多様な機能を持ち，また解の導出速度が速く正確である．文（ 2 ） 手順 1 で生成した PDG よりインバリアントカバレッ

法は SMT-lib2.0standard 言語 (以下 SMT 言語という) に従う．

ジに影響を及ぼす 1 実行パスを取得する．

2. 8 既 存 手 法（ 3 ） 手順 2 で得られたパス集合を実行するための条件式を

本節では著者が所属する研究グループが提案しているテスト

SMT 言語の文法に変換する．

ケース生成手法の概要と課題点について述べる．

2. 8. 1 既存手法概要（ 4 ） SMT ソルバに入力し，パス実行条件を満たす変数割り当てを求める．

既存手法では以下の手順でテストケースを生成する．

（ 5 ） (2)-(4) をインバリアントカバレッジに影響を及ぼす全（ 1 ） 対象メソッドの PDG を生成するての実行パス候補分繰り返す．

（ 2 ） 手順 1 で生成した PDG よりインバリアントカバレッ（ 6 ） 変数割り当てからテストケースを求める．

ジを満たすパス p を１つ取得する．

3. 2 PDG から 1 実行パスの抽出（ 3 ） パ ス p を 通 る ト ラップ 変 数 を 適 切 に 埋 め 込 み ，

まず，対象メソッドに対し，MASU [17] を用いて PDG をESC/Java2 [2] を用いてそのトラップ変数の組み合わせが真に生成する．PDG を利用し，インバリアントカバレッジに影響ならない（すなわちパス p を通らない）という性質 sp を作る．

を及ぼす，すべての実行パスを取得する．実行パスの取得法は（ 4 ） ESC/Java2 を実行し，sp の反例を得る．この反例は次の通りである．まず PDG から，返り値にデータ依存をする

パス p を通る証拠となる．

ノードを取得する．次に変数定義が制御依存する式を取得する．

（ 5 ） 手順 4 で取得した反例を解析し，Daikon を用いる際制御依存する式中で使用されている変数に関しても，データ依に使用するテストケース生成に必要な，パス p を通る十分条件存・制御依存を取得する．取得した変数定義を組み合わせて選を得る．

択することで実行パス候補を導出する．ただし，これらの実行（ 6 ） (2)-(5) をインバリアントカバレッジを満たす全てのパパスが実際に実行可能かどうかは，パスを抽出した時点では不ス候補だけ繰り替えす．

明である．

（ 7 ） テストケースを実行するときは制約を満たす値を乱択

3. 3 1 実行パスから SMT 言語への変換により導出し必要回数繰り返す．

入力を Java の 1 実行パスとし，出力を SMT 言語で表現さ

2. 8. 2 既存手法の課題点れたその実行パスを通るための変数割当を求める SMT 言語の既存研究には，反例から得られたテストケース制約が実際の式とする．本節では，変換規則の一部について説明を行っていパス実行条件より狭い．
この問題点は静的解析器である ESC/Java2 の反例出力を用いているために，実際のパス実行条件より狭いテストケース制約しか導出されないためおこる．

く．変換は抽出された実行パスの系列に対し行う．以下, 変換規則μを次のように与えるμ: EP → ES
ここで EP ，ES はそれぞれ，PDG の 1 ノードに相当する

Java の 文，SMT 言語への部分式である．

例えば， x>0 || y>0 が実際のテストケース制約であったと

3. 3. 1 変換補助関数

しても，x<=0 && y>0 が導出される場合がある．

変換に当たり，以下の補助関数を用いる．

このように実際より狭いテストケースしか生成されないため，（ 1 ） String name(String variable)

テストケースの質が下がり，結果表明の質が下がるという問題（ 2 ） String use(String variable)がある．

（ 3 ） String type(String Java type)

3. 提 案 手 法（ 4 ） int class(String className)（ 5 ） int point(String Instance)

2. 8. 2 小節であげた課題を解決するため，テストケース生成

補助関数 name とは，変数名 varibale を引数にとり，変数名手法に SMT ソルバ，Z3 を用いる．SMT ソルバでは反例としに ID をつけたものを返す．なお，ID は変数が更新された回数て制約を導出せず，パスの分岐条件そのものを用いてテストを表し，各変数ごとに ID を持つものとする．ID の初期値は 0ケースを求めるため，得られた制約が狭くなることはない．まである．すなわち，i 回値が更新されている変数が，name 関

た，SMT ソルバの解は制約ではなくその制約を満たす割り当数により呼び出されたときは，variable%i + 1 を返す．そしててを返すため，（７）のような乱択を再び繰り返すという無駄をその変数の ID をインクリメントする．

省ける．SMT ソルバを用いたテストケースの導出のためには，補助関数 use は，変数名 variable を引数にとり，変数名に ID

入力として SMT 言語で書かれた制約を満たすための式を与えをつけたものを返す．ID は変数が更新された回数を表す．すななければならない．そのために実行パス候補を SMT 言語で書わち，各変数の最新の値をかえす関数である．i 回値が更新されかれたパス実行条件の式への変換について実装した．これによている変数が，use 関数により呼び出されたときは，variable%i—3—表 1 Java 基本型と SMT 基本型の対応

Java:array Type array Name;Java の基本型 byte shortintchar long float double boolean

SMT 基本型

IntIntInt

Int

Int

RealReal

Bool

a[i];
a[i]=expression;
SMT:

Java:

Java:

integerExpression

realExpression

SMT:

SMT:

(to real integerExpression)(to int realExpression)(declareconst name(array Name) Array Int type(array Type))(select use(a) i)(assert (= (store use(a) i expression) name(a)))
図 4 配列の変換例

図 3 プリミティブ型のキャストの表現表 2 実験対象となるソースコードを返す．

プログラム名 行数

補助関数 type は，Java での変数の型 Java type を引数にとり，Calc

2123.5

Telephone2975.5Flower28419.5

JanCord26313

Operator

2163.7

RPS

1955Date28

95.4

それに対応する SMT 言語での型を返すものとする．
補助関数 class は，クラス名を表す変数 classN ame を引数にとり，クラスごとに定義しておいた固有の整数値を返す．
補助関数 point は，インスタンスを表す変数 Instance が何番目にインスタンス化されたかを返す関数である．
インスタンスが参照している場所を区別するために用いる．

3. 3. 2 変数の変換
SMT 言語では代入という概念が存在せず，式は等式か不等式でしか表すことができない．よって SMT 言語では同一の変実行パス候補数 平均パス長

Calc:2 次方程式の求解
Telephone:電話番号がどの種別を表すかの判定
Flower:窓辺の花 [19] のプログラム
JanCord:8 桁のバーコードチェックディジットが正しいかを判定する
Operator:演算子を表す文字を与えたとき，対応する演算を行う
RPS:じゃんけんの判定
Date:二つの日付のうちどちらが新しいかの判定数名であっても，変数の後に連番をつけることで区別をする．
className

そこで前述の補助関数 name, use を用いる．

ftype fieldName;

3. 3. 3 プリミティブ型の対応…

Java プログラムにおいて，定義される変数は SMT-LIB で

rType methodName(pType parameterName);は表 1 のように表す．ここで java type は Java プログラムで…の型，variable name は変数名，smt type は SMT-LIB での図 5 定義対象クラスの UML 表現

型を表す．

3. 3. 4 式 の 変 換Java:

本節では代入以外の式の変換方法について説明する．Java 演className oName = new className();

算子の優先順位に従って，前置記法で表現する．例えば 1+2∗x のoName.ftype;ような変換は演算子の優先順位にしたがい，(+ 1 (∗ 2 use(x)))

SMT:のように変換される．

(declare-datatypes () ((mk-obj (field (fieldName type(ftype))

3. 3. 5 プリミティブ型のキャスト変換
Java 言語では整数と実数の演算が可能であるが，SMT 言語(%pointer Int) (%class Int)))))(declare-const name(oName) type(className))(assert (= (%pointer use(a)) point() ))では整数と実数の演算は不可能である．例えば Java では 1+1.0(assert (= (%class use(a)) class(className)))などは自動でキャストされるが，SMT 言語では 1+1.0 のよう(fieldName use(oName))に型の違う演算を行うとエラーを出力する．そこで，整数を実

図 6 インスタンス化の変換数に変換する SMT 言語の関数 to real，to int を用いる．整数の部分式 integerExpression, 実数の部分式 realExpression

3. 3. 8 クラスのフィールドの変換はそれぞれ図 9 のように変換を行う．表 3 の左側をμの引数，まずクラスのフィールドを表すために，そのフィールドを持右側をμの返り値とする．

つレコードを定義しておく．図 5 のクラスがあるとき，インス

3. 3. 6 配列の変換

タンス化とフィールドの参照の変換方法は図 6 のようになる．

図 4 に 1 次元配列の宣言と使用, 代入についての変換を示す．

ここで，%pointer はインスタンスが参照している場所，%classはクラスの種類を表すものとする．以下，変換を表す図では上3. 3. 7 文字の変換
Java 言語では文字は文字コードを用いて整数として表すことができる．よって文字を表す char 型に関しては整数型 Int を段を変換規則μの引数とし，下段を変換規則μの返り値とする．
本変換により，既存の研究では表現できなかったクラスに対してもテストケースが導出できる．

用いて表す．String 型も同様に整数型の配列として表現する．

—4—

Java文法の式

SMT言語の式

int a,b,c,d;
int d = b * b - 4* a * c;not (d >= 0 &&a != 0);
return -1;(declare-const a%0 Int )(declare-const b%0 Int )(declare-const c%0 Int )(declare-const d%0 Int )(declare-const d%1 Int )(assert ( = d%1 ( - ( *b%0 b%0 ) ( * ( * 4a%0 ) c%0 ) ) ) )(assert ( and ( >= d%10 ) ( not (= a%0 0 )) ) )Java:method Name(parameter Name)
SMT:(declare-const name(methodName) type(method type))(declare-const name(instance) type(className))
図 7 メソッド起動式の変換

変換

Java:
variable type variable;variable = Expression;
SMT:

図 9 2 次方程式の解判定の変換(declare-const name(variable) type(variable type))
表3(declare-const name(variable) type(variable type))

実験結果(assert (= use(variable) Expression))
図 8 代入文，宣言文の変換プログラム名 実行時間 (秒) インバリアントカバレッジ

テストケース数

Calc28.6

100

40

Telephone

23.4

92

26

3. 3. 9 メソッド起動式の変換

Flower631.5

100

29

式中でメソッドを呼び出すときの変換方法について述べる．

JanCord

161.2

10044

メソッドの返り値に関しては，厳密な値を求めようとすると，Operator

25.9

10038RPS

26.4

10034Date

29.8

100160

状態爆発を起こす場合がある．そのためメソッドの返り値は自由な値をとるものとする．void 型のメソッドに関しては，変換しない．図 5 のクラスのメソッド methodN ame の変換は，図7 のようになる．
この変数 name(methodN ame) を式中に使うことで，メソッドの返り値を表現する．既存研究ではうまく定めることができなかったメソッドの返り値を求解できる．またこのメソッドを呼出したインスタンス instance はメソッドによりフィールド値が変更される場合があるため，インスタンスそのものも更新している．

3. 3. 10 条件式の変換
条件文を condition としたときに，条件が真となるパスを通るときは，(assertcondition)

条件が偽となるパスを通るときは，変換することが可能になる．

3. 3. 15 変 換 例
変換例を図 9 に示す．この変換は 2 次方程式 ax2 + bx + c が実数解を持たないときの変数の割り当てを求める SMT 言語の制約式へと変換を行っている．なお，return 文は変換しない．

3. 4 SMT ソルバを用いたテストケースの導出
制約を表す式が得られた後，満たす割り当てを SMT ソルバで求解する．この処理により，パスの実行可能性と，実行可能な場合の変数への割り当てを求めることができる．引数が以前求めた値と異なるという条件を加えて繰り返し実行することにより，同じ実行パスを通る複数の変数への割り当てを求めることができる．与えるテストケースの数が多いほど Daikon では質の高い表明を導出できる．

(assert (not condition))と変換をおこなう．

3. 3. 11 変数宣言の変換
変数名を variable，変数の型を variable type とすると，変数宣言は図 8 のように変換を行う．

3. 3. 12 代入文の変換
変数名を variable，変数の型を variable type とし，代入する式を Expression とすると，代入文は図 8 のように変換する．

3. 3. 13 if,while,for 文の変換
if 文は PDG 上では分岐条件のみ与えられ，その分岐条件が真となるパス，偽となるパスをそれぞれ取得することで対応する．while 文と for 文は任意の整数回だけループするようにパスを展開し，そのパスそれぞれに対して変換を行うことで対応する．

3. 3. 14 複文の変換
PDG から得た実行パス系列に対し，本稿で示してきた変換
規則μを各文ごとに順に適応していくことにより，複文全体を4. 評 価 実 験
本章では，評価実験の結果および考察について述べる．本研
究では評価実験として，手法を実装したツールを本章にて示すJava プログラムに対して適用した．本ツールを実行時間及び出力結果の妥当性の観点から評価を行う．

4. 1 評価実験の目的
本提案手法が実プログラムにおいて適用可能な範囲や，テストケースがインバリアントカバレッジを満たすための妥当な値であるかを様々なプログラムを対象に適用実験を行った．

4. 2 実 行 環 境
実行環境には，Intel(R) Core(TM)2 Duo CPU U9300 1.20GHz

Memory:2.00GB,Windows Vista,JDK1.6_17 および Z3-3.2 を使用した．

4. 3 適 用 対 象
本稿における実験対象を表 2 に示す．これらのソースコード—5—

の一部は本研究グループの行った既存研究 [18] でも実験対象としている．また，既存手法では本来より狭いテストケース制約を導出する実験対象となっている．

[4]

4. 4 実験の手順と結果提案手法から得られたテストケースのインバリアントカバレッジと実行時間，テストケース数を計測する．また得られた[5]

テストケースから既存手法で得ることのできないテストケースがあるかを調査する．実験結果として，表 3 の結果が得られた.

[6]

なおテストケース数は，値の同じテストケースは一つとして数える．

4. 5 考察[7]

提案手法で生成したテストケースが既存手法で導出できるかについて考察を行う．例として，flower というプログラムでは既存手法では 0 <= num <= 3 の否定から num >= 4 というテ[8]ストケース制約を得られたが，これは num < 0 というテストケース制約が抜けているため，制約としては不十分であり，Daikon で正しく表明を生成できない．しかし，本提案手法で[9]は，num = −1, a[0] = true など既存手法では生成できないテストケースを得られた．また，このテストケースは表明の生[10]

成をするうえで有用である．Telephone のインバリアントカバ
レッジが 100%でないのは，提案手法ではメソッドの返り値を任意の値を返すと定義していたり，配列の長さを SMT では求めることができないためである．実行時間に関しては現実的な実行時間でテストケースを生成することができたといえる．実行時間は PDG の生成と SMT ソルバの求解が大部分を占めて[11][12][13]いる．本手法では実行時間はパス数や生成したテストケース数，平均のパス長に依存している．既存手法との比較として，テス[14]トケース制約の広さの点から提案手法がよりメソッドの状態を詳しく表す表明を生成するために必要なテストケースを生成可能であるといえる．

[15]

5. あ と が き
本研究では我々の研究グループが提案している，表明自動導[16]出手法のためのテストケース生成手法の提案とその評価実験を行った．提案手法では，SMT ソルバや，PDG を利用してテストケース依存問題を解消している．その結果，既存手法で導出できなかったテストケースを導出できた．しかし，適用クラス[17]の狭さが課題点である．今後は適用可能なクラスを拡張し，その評価実験を行うことで本手法の有用性を評価していきたい．

謝

[18]

辞本研究の一部は科学研究費補助金基盤 C（21500036）と文部科学省「次世代 IT 基盤構築のための研究開発」（研究開発領域[19]

tended static checking,”, Compaq SRC Research Report,
1998.
M.D. Ernst, J.H. Perkins, S.M. P. J. Guo, C. Pacheco, M.S.
Tschantz, and C. Xiao, “The daikon system for dynamic
detection of likely invariants,” Science of Computer Programming, vol.69, no.1-3, pp.35–45, 2007.
M.D. Ernst, “Dynamically discovering likely program invariants,” Ph.D., University of Washington Department ofComputer Science and Engineering, Seattle, Washington,
Aug. 2000.
J.W. Nimmer, and M.D. Ernst, “Static verification of dynamically detected program invariants: Integrating daikonand ESC/Java,” in Proc. of First Workshop on RuntimeVerification, RV 2001, pp.152–171, 2001.
J. Ferrante, K.J. Ottenstein, and J.D. Warren, “The program dependence graph and its use in optimization,” ACM
Trasactions on Programming Languages and Systems, vol.9,no.3, pp.319–349, 1983.
N. Gupta, and Z.V. Heidepriem, “A new structural coverage criterion for dynamic detection of program invariants,”
in Proc. of Int. Conf. on Automated Software Engineering,ASE 2003, pp.49–58, 2003.
N. Gupta, “Generating test data for dynamically discovering likely program invariants,” in Proc. of ICSE 2003 Workshop on Dynamic Analysis, WODA 2003, pp.21–24, 2003.
L. De Moura, and N. Bjørner, “Satisfiability modulo theories: introduction and applications,” Commun. ACM,vol.54, pp.69–77, Sept. 2011.
梅村晃広，“SAT ソルバ・SMT ソルバの技術と応用”, コンピュー
タソフトウェア，vol.27，no.3，pp.24–35，2010．
D.R. Cok, “The smt-lib v2 language and tools: A tutorial,”
GrammaTech, 2011.
小林和貴，宮本敬三，岡野浩三，楠本真二，“表明動的生成を目的としたテストケース制約の ESC/Java2 を利用した導出”, ソ
フトウェア工学の基礎 XVII 日本ソフトウェア科学会ソフトウェ
ア工学の基礎ワークショップ FOSE2010，pp.35–44，2010．
J.W. Nimmer, and M.D. Ernst, “Invariant inference forstatic checking: An empirical evaulation,” in Proc. of SIGSOFT Symp. on Foundations of Software Engineering 2002,
FSE 2002, pp.11–20, 2002.
C. Flanagan, and K.R. Leino, “Houdini, an annotation assistant for ESC/Java,” in Proc. of Int. Symp. of FormalMethods Europe on Formal Methods for Increasing Software Productivity, FME 2001, pp.500–5178, 2001.
L. De Moura, and N. Bjørner, “Z3: An Eﬃcient SMT SolverTools, and Algorithms for the Construction and Analysis ofSystems,” vol.4963/2008, chapter 24, pp.337–340, Lecture
Notes in Computer Science, Springer Berlin, Berlin, Heidelberg, April 2008.
三宅達也，肥後芳樹，楠本真二，井上克郎，“多言語対応メトリ
クス計測プラグイン開発基盤 MASU の開発”, 電子情報通信学会論文誌 D，vol.J92-D，no.9，pp.1518–1531，2009．
宮本敬三，堀直哉，岡野浩三，楠本真二，“Daikon 生成表明改
善のためのテストケース自動生成手法とその評価実験”, 日本ソ
フトウェア科学会誌コンピュータソフトウェア，vol.28，no.4，pp.306–317，2011．
産業技術総合研究所システム検証研究センター, “4 日で学ぶモ
デル検査 (初級編)(CVS 教程 (1))”, エヌティーエス, 2006.

名：ソフトウェア構築状況の可視化技術の普及）の助成による．
文

献[1] B. Meyer, “Applying Design by Contract,” in Computer(IEEE), vol.25, no.10, pp.40–51, 1987.
[2] C. Flabagan, K. Rustan, M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata, “Extended static checking forJava,” Proc. of the ACM SIGPLAN 2002, pp.234–245, 2002.
[3] D.L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe, “Ex-—6—