日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

プログラム言語の標準解釈系上での記号実行のためのフレームワーク服部 哲
計算機プログラムの記号実行を，言語の標準解釈系上で行うためのフレームワークを提案する．プログラム中の数値
変数を，記号変数のオブジェクトに置き換える．プログラムにおける実行経路を，各比較演算の取るべき真偽値の列で指定する．各記号変数は，起動する比較演算のメソッドにおいて，自身の持つ数式と引数の持つ数式，および，取るべき真偽値により不等式を生成して経路条件に追加する．プログラムの実行後に得られる経路条件が充足可能ならば，記号変数による比較演算の系列と同じ真偽値の列を持つ，数値変数による比較演算の系列が存在する．本フレー
ムワークの意義は，(1) 記号実行の機構をオブジェクトに込めることにより，言語がオブジェクトを取り扱う諸機能をプログラムにおいて利用できること，(2) クラスライブラリ方式のため多くのオブジェクト指向言語が対象になること，また，ライブラリは簡潔であり容易に実装できること，(3) 単体テストのためのフレームワークなどと組み合
わせて利用できること，以上である．本論文では，プログラム言語 Scala に対する，フレームワークのクラスライ
ブラリの構築について述べる．Scala は演算子多重定義の機能を持つので，記号変数に対する比較演算を，プリミ
ティブ型に対する比較演算子を用いて定義できる．このことにより，プログラムに対する記号実行のための改編は，前記の通りの変数の置換えのみでよい．

のとする．従来のアプローチでは，記号実行に必要な1 はじめに実行経路や経路条件の情報は解釈系上に設けられる．

計算機プログラムのテスト [3] [12] のための技術の対象の言語の各構文に対しての，これらの情報を参一つとして，記号実行 (symbolic execution) が古く

照，更新する解釈規則を定めることにより，解釈系はから知られている [10] [18]．現在，ソフトウェア工学

構築される．このようなアプローチの利点は，特別なに関する国際会議 ICSE で記号実行のセッションが解釈系において記号実行の効率を追求できることや，設けられているように，注目度の高い技術である標準の解釈系では行えない実行方法も取れることで[1] [4] [5] [13] [19]．本論文では，記号実行に対する新しある．しかし，現在のプログラム言語は多機能で多くいアプローチとして，言語の標準解釈系上で記号実の構文を持つため，このような解釈系を新規に開発す行を行うフレームワークを提案する．また，具体的なるコストは大きい．

プログラム言語として Scala を取り上げ，フレーム本論文で提案するフレームワークでは，プログラ

ワークのクラスライブラリの構築について述べる．

ムの記号実行を，言語の標準の解釈系上で行う．記号

記号実行に対する従来のアプローチは，対象の言語

実行の対象の数値変数を，記号変数のオブジェクトにごとに，記号実行のための特別な解釈系を開発するこ置き換える．記号実行に必要な情報は，全てこのオブとによっている．ここで，プログラム言語に対する解

ジェクトに内包される．各記号変数は値として数式を釈系とは，コンパイラやインタプリタを総称したも持ち，また，記号変数間の共有情報として，実行経路

A Framework for Symbolic Execution on Standard Interpreters of a Programming Language
Satoshi Hattori (satoshi@cs.titech.ac.jp), 東京工業大学
情報理工学院, School of Computing, Tokyo Instituteof Technology.

を真偽値の列で表したものと，経路条件の不等式系とを持つ．プログラム中では，記号変数が比較演算のメ
ソッドを起動する．標準解釈系は，メソッドを起動した変数の持つ数式，引数の変数の持つ数式，比較演算

の取るべき真偽値を示すビット，以上から不等式を生のクラスから成る．(1) 数値変数 (Standard) クラス．

成して，経路条件に追加する．

数値のプリミティブ型，例えば Long や Double のラッオブジェクト指向言語が持つ機能は，データとして

パークラスである．次の記号変数クラスは，このクラのオブジェクトを管理 (例えばコレクション) し，まスを継承する．プリミティブ型の変数の代わりにこのた，データに対する計算を制御 (例えばメソッドの再クラスの変数を用いることで，記号実行時の変数の置

帰呼び出し) するものと言える．本フレームワークで換えの容易化を図る．(2) 記号変数 (Symbolic) クラ

は，記号実行の機構をオブジェクトに込めている．そス．フィールドとして，変数の値である数式，および，のため，プログラムにおいて上記のような機能を用

変数間の共有情報を持つ．継承する数値のフィールド

いた上で，標準解釈系上での記号実行が可能である．

は，数式値を経路条件の充足解で数値化したものとし

また，提案するフレームワークは，多くのオブジェクて用いる．(3) 数式 (Expression) クラス．記号変数

ト指向言語において，後述の各クラスを含むクラスラの取る値のクラスである．本論文では，数式は線形式

イブラリを実装することで利用できる．なお，このラであるとする．(4) 記号変数間の共有情報のクラス．

イブラリを，記号実行のための特別な解釈系とみなす

トレース (Trace) クラスと呼ぶ．フィールドとして，こともできる．しかし，ライブラリの行数は数百行程実行経路を表現するビット列と，経路条件を表現する度であるので，開発のコストは小さい．

不等式系などを持つ．(5) 不等式系 (Inequalities)

記号実行に対する従来のアプローチのうち，具体的な数値をプログラムに与える方式でない解釈系は，

クラス．線形不等式系の充足可能性判定を，ソルバー

Z3 [21] で行う．

静的解析のシステムに近いといえる．本フレームワー

本論文では，プログラム言語 Scala に対する，上記

クは，やはり具体的な数値をプログラムに与えないのクラスライブラリの構築について述べる．Scala をアプローチであるが，標準解釈系を用いる点では，動取り上げる理由は，一つは演算子多重定義 (operator

的解析のアプローチだと言える．プログラムのテス

overloading) の機能を持つこと，もう一つは，プログトに関して，単体テストのためのフレームワーク，例

ラムが Java 仮想機械 (JVM) 上で動作することであ

えば Java のための JUnit [9] などは普及しているとる．演算子多重定義により，記号変数クラスにおける言える．本フレームワークのもう一つの利点は，この比較演算のメソッドを，プリミティブ型に対する比較

ような単体テストのためのフレームワークなどと組演算子を用いて定義できる．このことにより，プログ

み合わせての利用が可能なことである．例えば，次のラムに対する記号実行のための改編は，前記の通りのように用いる．テストプログラムにおいて，テスト対変数の置換えのみでよい．また，プログラムが JVM

象のオブジェクトを，数値変数を記号変数のオブジェ上で動作するので，先述のフレームワーク JUnit や，

クトに置き換えて構成する．テストプログラムにルー

ソルバー Z3 の Java API を利用できる．

プを設け，ループ内にテスト対象のメソッドとアサー

本論文の構成は以下の通りである．第 2 節で，提ションのメソッドとを置く．経路条件が充足可能な場

案するフレームワークに関する概説を行う．既存のア合に限り，アサーションの検査を行う．アサーション

プローチとの比較，フレームワークの適用範囲，使用が満たされれば，クラスライブラリの機能によって次法について述べる．第 3 節で，フレームワークを形の実行経路を決定し，ループの先頭に戻る．全ての場式モデルにより定義する．第 4 節で，このモデルを合でアサーションが成立すれば，対象のメソッドの正例題を用いて説明する．第 5 節で，Scala 言語上でのしさが証明される．アサーションを満たさない経路がクラスライブラリの構築について述べる．第 6 節で，見つかれば，テストプログラムは終了する．このときScala プログラムの例題を取り上げ，フレームワークの経路条件の充足解は，数値変数でテストをする場合を用いた記号実行によるテストについて説明する．最のアサーションの反例となる．

後に，第 7 節で，今後の課題などについて述べる．

フレームワークのクラスライブラリは，次の 5 つ抽象化している．このため，解釈系 F は，単一の規2 フレームワークに関する概説

則による F = {(σ, s, Q) →c (σ, s′ , Q′ )} で定義され本節では，まず，記号実行のための既存のアプロー

る．ここで，c は比較文である．比較文においては，

チと，本論文の提案するフレームワークとの比較を行

数式値 σ は変化しない．しかし，Q に追加する不等う．続いて，本フレームワークの適用範囲と使用法に式の生成に必要なので記している．

ついて述べる．

比較文 c を，本論文では c = ▷◁ (p, q) と記す．ここに，▷◁ は任意の比較演算子，p, q は記号変数 (また2. 1 記号実行の方式の抽象的表現

は記号変数による式) である．このとき，▷◁ をプロ

プログラムの記号実行を，ホーア論理の拡張 [2] とグラムにおける比較演算のメソッドに，p をこのメの関連で述べる論文では，記号実行の解釈系の形式

ソッドを起動する記号変数に，q をメソッドの引数のモデルが示されることが多い．例えば，Separation

記号変数に，それぞれ対応付ける．p, q はそれぞれLogic の拡張を扱った文献 [17] に洗練されたモデルがの数式値である，σ(p), σ(q) を内包する．また，各記見られる．そのようなモデルでは，記号実行におけ号変数は，共有情報として s, Q を内包する．そして，る諸情報を symbolic state として表現する．そして，σ(p), σ(q), s に基づいた不等式を Q に追加する操作

それがプログラム中の式の評価，文の実行でどのようを，比較演算のメソッド ▷◁ に内包させる．従って，本に変化するかを，式や文の構文定義ごとの解釈規則と論文の場合は，解釈系として標準解釈系を用いること

して与える．記号実行のための解釈系を，ここでは，ができる．

このような解釈規則の集合として抽象的に表現する．

プログラムにおいては，比較文のみが経路条件の更各プログラム変数の初期値を，仕様変数 [7] (あるい新に関わる．比較演算の各時点での記号変数の数式値

は symbolic value [4]) という特別な記号で表す．任意の情報は必要であるが，時点間の数式値の変化の情報の時点のプログラム変数は，仕様変数に関する数式は不要である．よって，プログラムにおいて記号変数の値を取る．このため，ここでは，プログラム変数をの数式値 σ を変化させる構文要素，例えば代入文は，

記号変数と呼ぶ．記号変数の値を，変数名から数式へ

本フレームワークのモデルには含める必要がない．

の写像として形式化する．本論文では，記号実行に

経路条件の不等式系 Q の充足可能性判定は考慮における諸情報として，各記号変数の数式値 σ ，実行経入れる．すなわち，記号変数の数式値を線形式に限る

路 s(比較演算の結果の真偽値のビット列)，経路条件

ことにより，経路条件 Q を線形不等式系とする．こQ(不等式の集合)，以上のみを取り扱う．既存のアプのため，記号変数に対する算術演算を，加算と定数倍ローチで取り扱う情報がこれらのみであるという抽に限定する．いま，Q の充足解の一つを，仕様変数

象化の仮定を置き，本論文のアプローチとの比較をの集合から数の集合への写像 ρ で表す．ある時点の行ってみる．

記号変数の数式値の写像 σ と，写像 ρ の合成写像をプログラムにおける構文の集合を P ，P の任意の

τ = ρ ◦ σ とする．プログラムの数値実行では，同じ要素を c と置く．すると，記号実行のための解釈系 F

時点のプログラム変数の値が，写像 τ による数値で′は，F = {(σ, s, Q) →c (σ , s , Q ) | c ∈ P } で定義さ与えられる．この場合のプログラム変数を，数値変数れる．記号変数の数式値は，代入演算などの場合に，

と呼ぶ．

′

′

′

σ から σ へと変化する．また，比較演算などの場合に，実行経路 s は，真偽値の使用によって s′ に変化

2. 2 本フレームワークの適用範囲

する．同じく，経路条件 Q は，新たな不等式の追加提案するフレームワーク (FW) と，本論文での′により Q に変化する．
本論文における記号実行では，実行経路 s と経路条件 Q を変化させる構文要素は，比較文のみであるとScala 言語に対するクラスライブラリ (CL) とに分けて，記号実行の対象を列挙していく．

• 対象のプログラム言語

(FW) オブジェクト指向言語で，演算子多重定義(CL) 数値型として，Long 型，または，Doubleの機能を持つものを対象とする．プログラム変数型を用いることができる．Long 型と Double 型

を，数値変数クラスと記号変数クラスの両者で表とを混合して用いることはできない．経路条件の現する．数値変数クラスを，数値のプリミティブ

線形不等式系は，ソルバー Z3 で充足可能性を判型のラッパークラスとする．記号変数クラスは数定する．Z3 では，制約記述において整数型と実値変数クラスのサブクラスであり，数値のフィー数型とを混合することができない．プログラムでルドに加えて，数式値および共有情報のフィール

は混合を許し，Z3 に入力する制約記述の生成のドを持つ．

際に，整数型を実数型に変換するという方針を取両クラスに，算術演算と比較演算のメソッドを設ることは不可能ではない．しかし，現状のクラス

ける．演算子多重定義により，各演算のメソッド

ライブラリでは，型の混合はしないという方針を

を，数値のプリミティブ型に対する演算子で定義取っている．

する．プログラムを数値変数クラスのインスタン• 対象とする網羅性

スを用いて記述すれば，記号実行のためのプログ(FW) プログラム中の数値変数に関する比較演算

ラムの改編は，数値変数の記号変数への置換えのについて，その真偽値の網羅を行う．

みでよい．なお，演算子多重定義の機能がない場• 対象の算術演算

合についての補足は，後で行う．

(CL) 記号変数クラスの算術演算として，加減算

なお，オブジェクト指向言語が，手続き型であると定数倍のみを対象とする．この結果，記号変数

か，関数型であるかは問わない．これは，記号変の数式値は線形式となる．従って，経路条件は線数の数式値を変化させる構文要素，例えば代入文

形不等式系となり，充足可能性を決定できる．

などを，フレームワークのモデルが含まないこと

数値変数クラスの算術演算も，加減乗算を対象による．

とする．これは，Scala に対するクラスライブラ

既に述べている通り，本論文では Scala を対象

リの，現在の実装に起因する．プリミティブとしの言語としている．

て Long 型と Double 型の両者を対象とするので，• 対象の変数scala.math.Numeric クラスを使った実装を行っ(CL) オブジェクト指向言語のプログラムにおけている．どちらかのクラスに限定すれば，除算もる，フィールドを対象とする．対象クラスのコン対象としたライブラリとすることができる．

ストラクタの引数で，フィールドのインスタンス• 対象とするプログラムの構文を与えられる場合には，コンストラクタの引数で(FW) 本フレームワークの原理により，全ての構

記号変数を与える．そうでない場合には，記号実文が対象となる．記号変数をコレクションの成分

行用の別のコンストラクタを記述し，それによりとしたり，記号変数に関する計算をループや再帰フィールドを記号変数とする．これらの方法によ呼び出しを用いて行ったりすることができる．

り，一つの対象プログラムに対する，通常の数値(CL) 記号変数クラスの比較演算は，コンパレー

変数による実行と，テスト時の記号変数による実タの記述によるものではない．これにより，コレ行とが可能になる．

クションに対するコンパレータを用いたソーティ• 対象の変数の型

ングのメソッドは，用いることができない．

(FW) プリミティブの数値型のラッパークラスを
数値変数クラスとする．本フレームワークでは，

2. 3 クラスライブラリの使用法

記号変数の起動する比較演算のメソッドが経路

プログラム言語 Scala に対する，フレームワー

条件の更新を行う．この原理により，プリミティ

クのクラスライブラリの使用法を説明する．ライブの論理型は対象にできない．

ブラリは，次の 5 つのクラスから成る．数値変数

(Standard) クラス，記号変数 (Symbolic) クラス，数する．

式 (Expression) クラス，トレース (Trace) クラス，

• 実行経路を指定する．単一の経路の指定と，全線形不等式系 (Inequalities) クラス，以上である．

ての実行経路の網羅の指定とができる．プログ

記号変数クラスは，数値変数クラスのサブクラスであ

ラムは，「ガイド」に従って実行する．トレース

る．各クラスは，数のプリミティブ型のクラス K を型

クラスのフィールド guide が，ガイドを表現すパラメータとして取る．クラス K として，Long 型とる．これは，整数型のリストであり，各比較演算

Double 型とが使用可能である．本節では，Long 型をの取るべき真偽値である，ビット 0 または 1 を用いる場合の説明を行う．なお，線形不等式系クラスに成分とする．単一の経路の指定の場合，フィー

おいて，ソルバー Z3 を用いる．Z3 の使用には，Java

ルド guide のリストを直接与える．なお，形式API を提供するファイル com.microsoft.z3.jar，

モデルにおけるガイドに対して，実装におけるおよび，実行時リンクのファイル (Windows の場合

guide はその逆順のリストである．

libz3.dll, libz3java.dll) が必要である．

全ての実行経路の網羅を指定する場合，初期ガイ

以下，Scala プログラムの記号実行によるテストのドとして，トレースクラスのコンストラクタが設ために行うべきことを，順に記述する．第 6 節の，例

定するガイドを用いる．実行経路の網羅の方法は題による説明も参照されたい．

後述する．

• 記号実行の対象プログラムの改編について述べる．
対象とするクラス中の，対象の Long 型のフィール• 対象クラス中の，記号実行の対象メソッドを起動する．

ドを，数値変数型，すなわち，Standard[Long]• 対象メソッドに対するテストを行う．テストは，型に改編する．このフィールドがメソッド中の局

経路条件が充足可能な場合にのみ行う．トレース

所変数に代入されている場合などは，局所変数のクラスのフィールド condition が，経路条件を型も変更する．開発環境を用いれば，このような表現する．同クラスのフィールド sat, solution

変更は容易である．

は，それぞれ，経路条件の充足可能性と充足解と• 以降は，記号実行によるテストプログラムの記を表現する．プログラム変数の初期値に関する述法である．記号変数クラスのインスタンスの生

テストの場合，solution の成分に対するアサー

成には，トレースクラスのインスタンスが必要

ションを記述する．プログラム変数の現在値に関である．ここでは，インスタンスを trace とし，するテストの場合，記号変数の数式値を初期値にトレースクラスのコンストラクタ起動 trace =よって数値化する．これは，記号変数クラスのメ

new Trace[Long](0) により生成する．引数の 0

ソッド instanciate で行うことができる．

は，ソルバー Z3 に対して整数型を用いることを• 全ての実行経路の網羅を指定する場合，上記の指示する．プリミティブとして Double 型を用いようなテストが成功すれば，次の実行経路に対る場合は，引数を 1 として，実数型を用いるこするテストを行う．トレースクラスのメソッドとを指示する，nextGuide は，現在のガイドを次のガイドに更• 対象クラスのコンストラクタで，対象のフィール

新する．このメソッドは，次のガイドの存在を

ドに，記号変数型，すなわち，Symbolic[Long]

表現する，同クラスのフィールド hasNextGuide

型のインスタンスを与える．これは，適用範囲のの更新も行う．よって，ループの実行条件を，こ部分で述べた通りの方法で行う．コンストラクタのフィールドの値が true であることとして，メの引数でフィールドのインスタンスを与えられる

ソッド起動，テスト，ガイドの更新，以上を繰り場合には，コンストラクタの引数で記号変数を与返す．

える．そうでない場合には，別のコンストラクタ

以上が，クラスライブラリの基本的な用法である．

を記述し，それによってフィールドを記号変数とオプション的な事項は，ライブラリの構築についての

a0 , a1 , · · · , an ∈ K である．ベクトル (a0 , a1 , · · · , an )節で述べる．

を，t の係数列と言う．

3 フレームワークのモデル定義

命題 1 集合 E = {e1 , · · · , en } を仕様変数の集合とフレームワークの形式モデルによる定義を行う．前する．このとき，任意の数式 t ∈ K[E] は，K 上の計

節の，フレームワークの抽象的な表現における記法を算によって，正規形 t = a0 + a1 ∗ e1 + · · · + an ∗ en

承けている．

で表すことができる．ここに，a0 , a1 , · · · , an ∈ K である．

3. 1 変数と算術演算(証明) K[E] の要素の定義に合わせて場合分けする．

定義 1 集合 K を，加算と乗算について閉じた数の′集合とする．すなわち，任意の a, a ∈ K に対し，′′

a + a , a ∗ a ∈ K である．
次に定義する仕様変数は，プログラム変数の初期値を表す特別な変数である．

• t = a ∈ K は，正規形で a0 = a，および，各i(1 ≤ i ≤ n) について ai = 0 としたものである．
• t = ek ∈ E は，正規形で a0 = 0, ak = 1，および，各 i(1 ≤ i ≤ n, i ̸= k) について ai = 0 としたものである．

定義 2 仕様変数は，集合 K の要素を値として持つ変• t = u + w, u, w ∈ K[E] について，u = a′0 + a′1 ∗数である．集合 E = {e1 , · · · , en } を仕様変数の集合

e1 +· · ·+a′n ∗en , w = a′′0 +a1′′ ∗e1 +· · ·+a′′n ∗en ととする．各仕様変数 ei ∈ E(1 ≤ i ≤ n) は，与えられ

′
′′
′
′′
仮定する．ここに，a′0 , a′′
0 , a1 , a1 , · · · , an , an ∈ K

た写像 ρ : E → K によって定められる数 ρ(ei ) ∈ K

で あ る ．こ の と き ，K 上 の 計 算 に よ り，t =を値とする．

(a′0 + a′′0 ) + (a′1 + a′′1 ) ∗ e1 + · · · + (a′n + a′′n ) ∗ en

集合 E 上の算術演算を，E 上の数式の定義によって与える．なお，数式は線形式とする．

とできる．

• t = a ∗ u, a ∈ K, u ∈ K[E] について，u =定義 3 集合 E = {e1 , · · · , en } を仕様変数の集合とす

a′0 + a′1 ∗ e1 + · · · + a′n ∗ en と仮定する．ここに，る．E 上の数式の集合 K[E] を，次の通り定義する．

a′0 , a′1 , · · · , a′n ∈ K である．このとき，K 上の計

また，E → K の任意の写像 ρ を，K[E] → K の写算により，t = (a ∗ a′0 ) + (a ∗ a′1 ) ∗ e1 + · · · + (a ∗像へと拡張し，数式 t ∈ K[E] の値 ρ(t) を定義する．

a′n ) ∗ en とできる．

• 数 a ∈ K に対し，a ∈ K[E] とする．t = a と置くとき，ρ(t) = a ∈ K とする．

• 仕様変数 ek ∈ E(1 ≤ k ≤ n) に対し，ek ∈ K[E]プログラム変数を，集合 E 上の数式，および，集合 K の要素である数の両者を値に持つ変数として定義する．

とする．t = ek と置くとき，ρ(t) = ρ(ek ) ∈ K

定義 5 プログラム変数は，集合 K[E] の要素であるとする．

数式，および，集合 K の要素である数の両者を値• 数式 u, w ∈ K[E] に対し，u+w ∈ K[E] とする．

として持つ変数である．集合 X をプログラム変数t = u + w と置くとき，ρ(t) = ρ(u) + ρ(w) ∈ Kの集合とする．いま，2 つの写像 σ : X → K[E] ととする．

ρ : E → K とが与えられたとする．写像 τ を，合成

• 数 a ∈ K, 数式 u ∈ K[E] に対し，a ∗ u ∈ K[E]写像 τ = ρ ◦ σ : X → K と定める．このとき，各プとする．t = a∗u と置くとき，ρ(t) = a∗ρ(u) ∈ K

ログラム変数 x ∈ X は，写像 σ によって定められるとする．

数式 σ(x) ∈ K[E]，および，写像 τ によって定めら集合 K[E] の要素である数式は，E の要素の線形

れる数 τ (x) ∈ K を値とする．数式 σ(x) を変数 x の結合に定数項を加えたものとして表すことができる．

数式値と，数 τ (x) を x の数値と，それぞれ呼ぶ．

定義 4 集合 E = {e1 , · · · , en } を仕様変数の集合とす

集合 E の場合と同様に，集合 X 上の数式値に関する．数式 t ∈ K[E] が t = a0 + a1 ∗ e1 + · · · + an ∗ en

る算術演算を，X 上の変数式の定義によって与える．

と表されるとき，t は正規形であると言う．ここに，

なお，変数式も線形式である．集合 K[E] の要素を数

式，集合 K[X] の要素を変数式と呼んで，両者を区別である．ベクトルのドット積を用いれば，τ (x) =する．

(a0 , a1 , · · · , an ) · (1, ρ(e1 ), · · · , ρ(en )) と表せる．

定義 6 集合 X, E を，それぞれプログラム変数の集プログラム変数を定義したので，プログラム変数の合，仕様変数の集合とする．X 上の変数式の集合

数式値の初期値を，仕様変数を用いて定義する．

K[X] を，次の通り定義する．また，X → K[E] の定義 8 集合 X をプログラム変数の集合，集合 E =任意の写像 σ を，K[X] → K[E] を満たす写像へと{e1 , · · · , en } を仕様変数の集合とする．ここで，X の拡張し，変数式 r ∈ K[X] の数式値 σ(r) を定義する．

要素数を n 以上とし，集合 P = {x1 , · · · , xn } ⊆ X• 数 a ∈ K に対し，a ∈ K[X] とする．r = a とを導入する．このとき，写像 σ0 : X → K[E] を，次置くとき，σ(r) = a ∈ K[E] とする．

• プログラム変数 x ∈ X に対し，x ∈ K[X] とする．r = x と置くとき，σ(r) = σ(x) ∈ K[E] とする．

• 変数式 p, q ∈ K[X] に対し，p+q ∈ K[X] とする．

の通り定義する．

• 各 i(1 ≤ i ≤ n) に対して，σ0 (xi ) = ei ∈ E ⊆K[E]．
• x ∈ X\P に対しては，σ0 (x) は未定義とする．
上記の定義から，σ0 は実際には部分写像である．

r = p+q と置くとき，σ(r) = σ(p)+σ(q) ∈ K[E]とする．

3. 2 変数と比較演算• 数 a ∈ K, 変数式 p ∈ K[X] に対し，a∗p ∈ K[X]数の集合 K について，以降では，全順序集合といとする．r = a ∗ p と置くとき，σ(r) = a ∗ σ(p) ∈う仮定を追加する．任意の比較演算子を ▷◁ で表し，

K[E] とする．

その否定の比較演算子を ¬ ▷◁ で表す．数 a, a′ ∈ K に

集合 X 上の数値に関する算術演算も，同様に定義

ついて，a ▷◁ a′ が真であることと，a(¬ ▷◁)a′ が偽でできる．

あることとは同値である．否定の比較演算子の見やす

定義 7 集合 X, E を，それぞれプログラム変数のさのため，以降では，前置記法 ▷◁ (a, a′ ), ¬ ▷◁ (a, a′ )集合 ，仕様 変 数の集 合 とする ．いま，2 つの写像を用いる．

σ : X → K[E] と ρ : E → K とが与えられたとする．

まず，仕様変数の集合 E 上の比較文を定義する．

写像 τ を，合成写像 τ = ρ ◦ σ : X → K とする．こ

本論文では，数学的な等価性や名前付けには記号 =のとき，写像 τ を，K[X] → K を満たす写像へと拡を用いている．比較文における等価演算子には ≃ を張し，変数式 r ∈ K[X] の数値 τ (r) を定義する．

用いて，これと区別する．

• r = a ∈ K に対し，τ (r) = a ∈ K とする．

定義 9 数の集合 K を，加算と乗算について閉じ• r = x ∈ X に対し，τ (r) = τ (x) ∈ K とする．

た 全 順 序 集 合 と す る ．集 合 E を 仕 様 変 数 の 集 合• r = p + q, p, q ∈ K[X] に対し，τ (r) = τ (p) +とする．集合 C を比較演算子の集合，すなわち，

τ (q) ∈ K とする．
• r = a ∗ p, a ∈ K, p ∈ K[X] に対し，τ (r) =a ∗ τ (p) ∈ K とする．
プログラム変数の数式値が正規形で与えられるとC = {≃, ≥, ≤, >, <, ̸≃} とする．C の任意の要素を記号 ▷◁ で表す．
このとき，集合 E 上の比較文の集合 K⟨E⟩ を，

K⟨E⟩ = {▷◁ (u, w) | ▷◁ ∈ C, u, w ∈ K[E]} と定きの，変数の数値を示す．

義する．また，比較文 ▷◁ (u, w) の否定の比較文を，

命題 2 集合 X, E を，それぞれプログラム変数の集¬ ▷◁ (u, w) と記す．

合，仕様変数の集合とする．与えられた 2 つの写像

集合 E 上の比較文の真偽値を，集合 K が全順序集

σ : X → K[E] と ρ : E → K とに対し，τ = ρ ◦ σ :合であることに基づいて定義する．ここでは，比較文

X → K とする．プログラム変数 x ∈ X の数式値がの真偽値を，ビットで与えることにする．後の定義のσ(x) = a0 +a1 ∗e1 +· · ·+an ∗en のとき，x の数値は，ために，ビット列も定義する．

τ (x) = ρ(σ(x)) = a0 + a1 ∗ ρ(e1 ) + · · · + an ∗ ρ(en )定義 10 整数の集合 B = {0, 1} を導入する．B の要素 0, 1 をビットと言う．
ビット列は，ビットの列である．長さ m のビット

構成 (c, σ; b) の定める比較命題 δ(c, σ; b) ∈ K⟨E⟩ を，下記の通り定める．

列 s を，s = (b1 , · · · , bm ) のように表す．ここに，• δ(c, σ; 1) = ▷◁ (σ(p), σ(q)) とする．

bj ∈ B(1 ≤ j ≤ m) である．ビット列全体の集合を• δ(c, σ; 0) = ¬ ▷◁ (σ(p), σ(q)) とする．

S とする．集合 S は，長さ 0 のビット列である，空比較構成 (c, σ; b) における写像 σ も，部分写像で列 ϵ を含むとする．

よい．すなわち，比較文 c に現れない変数の数式値は

定義 11 仕 様 変 数 の 集 合 E 上 の 比 較 文 d = ▷◁未定義でよい．

(u, w) ∈ K⟨E⟩ と，写像 ρ : E → K とが与えらプログラムの実行を，次のようにとらえる．時点

れたときの，d の真偽値 ϕ(d, ρ) ∈ B を定義する．

j の比較文 cj と写像 σj とに対し，真偽値 bj を与え，• 集合 K 上で ▷◁ (ρ(u), ρ(w)) ならば，ϕ(d, ρ) = 1とする．

• 集合 K 上で ¬ ▷◁ (ρ(u), ρ(w)) ならば，ϕ(d, ρ) =0 とする．
次に，プログラム変数の集合 X 上の比較文を定義する．

比較構成とする．真偽値 bj によってプログラムが続行し，時点 j + 1 の比較文 cj+1 と写像 σj+1 とが定まる．最後の比較構成における真偽値 bm によって，最後の写像 σm+1 も定まるが，これはモデルからは捨象する．
ここで，比較構成の系列を定義する．比較構成の系

定義 12 集合 K を数の集合，集合 X をプログラ列の定める命題は，比較命題の論理積である．

ム 変 数 の 集 合 ，集 合 C を 比 較 演 算 子 の 集 合 と す

定義 15 ビット列 s = (b1 , · · · , bm ) ∈ S が与えられる．このとき，集合 X 上の比較文の集合 K⟨X⟩ を，たとする．s に対して，プログラム変数の集合 X 上K⟨X⟩ = {▷◁ (p, q) | ▷◁ ∈ C, p, q ∈ K[X]} と定義の比較構成の列 (c1 , σ1 ; b1 ), · · · , (cm , σm ; bm ) が定まする．

るとする．このような，比較構成の列を定めるため

集合 X 上の比較文の真偽値も，プログラム変数ののビット列を，トレースと言う．整数 m を，トレー数値が与えられた場合には定義できる．

ス s のトレース長と言う．また，上記の比較構成の列

定義 13 プログラム変数の集合 X 上の比較文 c =を，トレース s の定める比較構成列 D(s) と言う．さ▷◁ (p, q) ∈ K⟨X⟩ と，2 つの写像 σ : X → K[E] とらに，次の集合 Q(s) を，トレース s の定めるトレーρ : E → K とが与えられたとする．写像 τ を，合成ス条件と呼ぶ．Q(s) = {δ(cj , σj ; bj ) | 1 ≤ j ≤ m}．

写像 τ = ρ ◦ σ : X → K と定める．このとき，c の真

集合 E 上の比較文は線形不等式だから，トレース

偽値 ψ(c, τ ) ∈ B を定義する．

• 集合 K 上で ▷◁ (τ (p), τ (q)) ならば，ψ(c, τ ) = 1とする．

• 集合 K 上で ¬ ▷◁ (τ (p), τ (q)) ならば，ψ(c, τ ) =0 とする．
集合 X 上の比較文の真偽値は，プログラム変数の条件 Q(s) は E 上の線形不等式系である．よって，充足可能性が決定可能である [6]．
定義 16 与えられたトレース s ∈ S が，比較構成列

D(s) とトレース条件 Q(s) とを定めるとする．集合E 上の線形不等式系 Q(s) が充足可能であるとき，任意の充足解 ρ : E → K を，トレース s に対する充足

数式値のみでは決定することができない．この場合に解と言う．

は，逆に，X 上の比較文に対して真偽値を与えたと

命題 3 ト レ ー ス s = (b1 , · · · , bm ) ∈ S が 与 え

きの，成立すべき命題を定義する．命題は集合 E 上

ら れ た と す る ．s の 定 め る 比 較 構 成 列 D(s) を ，の比較文となる．

(c1 , σ1 ; b1 ), · · · , (cm , σm ; bm ) とする．ここで，s の定義 14 プログラム変数の集合 X 上の比較文 c = ▷◁定めるトレース条件 Q(s) が充足可能であると仮定(p, q) ∈ K⟨X⟩，写像 σ : X → K[E]，および，ビッ

し，s に対する充足解を ρ : E → K と置く．いま，ト b ∈ B が与えられたとする．このとき，3 字組

各 j(1 ≤ j ≤ m) に対し cj = ▷◁j (pj , qj ) であるとし，(c, σ; b) を集合 X 上の比較構成と言う．また，比較τj = ρ ◦ σj と置く．すると，集合 K 上で，各 j に対

して次が成立する．

現在のクラスライブラリでは，ガイドを定義の逆• bj = 1 ならば，▷◁j (τj (pj ), τj (qj ))．

順のリストとして実装している．また，インデックス• bj = 0 ならば，¬ ▷◁j (τj (pj ), τj (qj ))．

を 0 開始としているので，定義で先頭 (0 番目) から(証明) 定義 14 により，トレース条件 Q(s) は，各

j − 1 番目のビット bj−1 は，逆順のリストの先頭から l − j 番目のビットとなる．

j について次の比較命題を含んでいる．
• bj = 1 ならば，▷◁j (σj (pj ), σj (qj ))．

次に，トレースの網羅のための諸定義を行う．

• bj = 0 ならば，¬ ▷◁j (σj (pj ), σj (qj ))．

定義 19 初期ガイド g ∈ S を，空列 g = ϵ とする．

写像 ρ は，各 j に対して比較命題を充足するから，

定義 20 ビット列 s = (b1 , · · · , bm ) ∈ S について，記本命題が成立する．

法 β(s) により，s の表現する 2 進数を表す．10 進値

定義 17 ト レ ー ス s = (b1 , · · · , bm ) ∈ S が 与 え

で書けば，β(s) =られたとする．s の定める比較構成の列 D(s) を，

数 z について，記法 α(z) により，z の表現するビッ(c1 , σ1 ; b1 ), · · · , (cm , σm ; bm ) と す る ．あ る k(1 <ト列を表す．

′∑mj=1

2m−j bj である．逆に，2 進k ≤ m) に対して，トレース s = (b1 , · · · , bk−1 ) と定義 21 ガイド g ∈ S と整数 h とが与えられたと

s′′ = (b1 , · · · , bk−1 , bk ) とを定義したとき，トレース

き，g に対する長さ h の次のガイド ν(g, h) ∈ S を，条件 Q(s′ ) が充足可能であり，かつ，トレース条件

ν(g, h) = α(β(θ(g, h)) + 1) と定義する．ただし，ト′′Q(s ) が充足不能であるとする．このとき，整数 k

レース θ(g, h) のビットが全て 1 の場合，ν(g, h) は定を，トレース s の切上げ長と言う．

義されないとする．
定義 18 により，ガイド g に対する次のガイドにお3. 3 ガイドとトレース

いて，末尾に連続するビット 0 は取り除いても差し

定義 15 で，トレースを導入した．以降では，ト

支えない．クラスライブラリでも，そのように実装しレースの決定と網羅に関する諸定義を行う．

ている．

プログラムの実行において出現する比較文の数，す定義 22 二分木 T が与えられ，T は節点の集合 V をなわちトレース長を，標準解釈系が前もって知ること持つとする．T の各節点 v ∈ V は，以下で定められはできない．そこで，プログラムには，ガイドと言うる，ビット列によるラベル λ(v) ∈ S を持つ．

任意長のビット列を与える．そして，与えたガイドに対して，トレースを次の通り決定する．ガイドの長• v が深さ 0 の節点，すなわち根節点であるとき，v はラベル λ(v) = ϵ を持つ．

さが比較文の数よりも小さければ，ガイドにビット 0• v が 深 さ j の 中 間 節 点 で ，ラ ベ ル λ(v) =を必要なだけ補って，すなわち比較演算の真偽値とし(b1 , · · · , bj ) を 持 つ と す る ．こ の と き ，v の 左て偽を取り続け，プログラムの実行を継続する．ガイの子節点 v0 は，ラベル λ(v0 ) = (b1 , · · · , bj , 0)

ドの長さが比較文の数よりも大きければ，余ったビッを持ち，v の右の子節点 v1 は，ラベル λ(v1 ) =トは使用しない．トレースは，このようにしてプログ(b1 , · · · , bj , 1) を持つ．

ラムを実行した後の，比較文の数と同じ長さのビット

定義 23 二分木 T が与えられ，T は節点の集合 V を列である．

持つとする．いま，ガイド g ∈ S が与えられたとす

定義 18 ガイド は 任意の ビット列である．ガイド

る．このとき，ある整数 m が存在して，T の葉節点

g = (b1 , · · · , bl ) ∈ S と整数 m とが与えられたとき，

v がラベル λ(v) = θ(g, m) を持つ．この葉節点 v を，

g に対するトレース長 m のトレース θ(g, m) ∈ S を，

ガイド g に対する T の葉節点と言う．

下記の通り定義する．

ガイド g に対する葉節点 (the leaf for a guide) の• m ≤ l ならば，θ(g, m) = (b1 , · · · , bm ) とする．
• m

図解を，図 1 に示す．

(b1 , · · · , bl ,トレースを網羅してのプログラムの記号実行は，次

bl+1 , · · · bm )，bj = 0 (l + 1 ≤ j ≤ m) とする．

の，二分木 T に対する葉節点の巡回手続きでモデル>

l な ら ば ，θ(g, m)=

䃔

4 バブルソートの例題
例 1 次のモデルプログラムは，3 数 x1 , x2 , x3 をバDELQDU\WUHH7

P

ブルソートによってソーティングするものである．

if (x1 > x2 ){y := x1 ; x1 := x2 ; x2 := y; }PDJXLGHJ

00

WKHOHDIYIRUJ䃚 Y  䃗 JP 
DJXLGHJ

図1

䞉
䞉
䞉
0

if (x2 > x3 ){y := x2 ; x2 := x3 ; x3 := y; }if (x1 > x2 ){y := x1 ; x1 := x2 ; x2 := y; }定義 5 で導入したプログラム変数の集合 X を，こWKHOHDIYIRUJ䃚 Y  䃗 JP 

こでは，X = {x1 , x2 , x3 , y} とする．定義 8 に従い，集合 P = {x1 , x2 , x3 } ⊆ X を導入し，仕様変数の集合を E = {e1 , e2 , e3 } とする．図 2 は，定義 22 で導The Leaf for a Guide

入した二分木 T である．各節点について，ビット列のラベルを示してある．なお，本節では，ビット列は化される．

括弧やコンマを用いずに，ビットの連接の形で記す．

定義 24 二分木 T が与えられ，T は節点の集合 V を

代入文は，前節の形式モデルには含まない．比較文の持つとする．このとき，T に対する葉節点の巡回手続前後に現れる代入文を，図の二分木 T の枝上に記しきを，次の通り定義するている．(∗) は代入文が存在しないこと，(∗∗), (∗ ∗ ∗)• まず，T に対して，初期ガイド g = ϵ を与える．g に対する T の葉節点 v を求める．いま，は記述された代入文の存在を示している．本節では，比較文で中置記法を用いる．

λ(v) = θ(g, m) であるとする．
• (∗) ガ イ ド g に 対 す る 長 さ m の 次 の ガ イ ドν(g, m) が存在しないならば，手続きを終了す

WKHYDOXHVDUH
QRWFKDQJHG[![る．存在するならば，次のガイド g ′ = ν(g, m)を得る．そして，g ′ に対する T の葉節点 v ′ を求′′′める．いま，λ(v ) = θ(g , m ) であるとする．こ′′こで，g = g , m = m とし，(∗) に戻る．
この手続きにおいて，求めた葉節点を巡回された葉節点と言う．また，葉節点のラベルの部分列をラベルに持つ節点を，訪問された節点と言う．
ここで，ガイド g に対する次のガイドを求める際，

\ [
[ [[ \\ [[ [[ \

䃔





[![[![









[![[![[![[![













 LQIHDVLEOH 





 LQIHDVLEOH 





長さ m の代わりに，定義 17 で導入したトレース

θ(g, m) の切上げ長 k を用いることもできる．この場

図2

Bubble Sort of Three Numbers

合の巡回手続きは，二分木 T の部分木に対するものとなる．

図で，T の各葉節点の下に，3 桁の数字を示してあ

命題 4 二分木 T が与えられ，T は節点の集合 V をる．この例では，葉節点 010 を取り上げる．定義 16 に持つとする．このとき，T に対する葉節点の巡回手続

従い，トレース s = 010 に対する充足解を ρ : E → K

きによって，T の全ての葉節点が巡回される．

と置く．このとき，関係 ρ(e1 ) ≤ ρ(e3 ) < ρ(e2 ) が成(証明) 任意のガイドに対する次のガイドは，二分立する．葉節点 010 の下の数字 132 は，このような木 T においてまだ訪問されていない節点のラベルで仕様変数の値の昇順の並べ替えを，添字を取り出してあることによる．

示したものである．

定義 18 のガイドとして，ビット列 g = 01 ∈ S

用いると，この不等式は e1 ≤ e3 となる．

が与えられたとする．ガイド g の長さは l = 2 で以上より，トレース s = 010 の定めるトレース条ある．定義に従い，ガイド g に対するトレースを，件を，Q(s) = {e1 ≤ e2 , e2 > e3 , e1 ≤ e3 } と得る．

長さ m を変化させて示す．長さ m = 1, 2 に対し，

線形不等式系 Q(s) は充足可能である．定義 16 の，m ≤ l である．よって，これらの長さのトレースは，

トレース s に対する充足解 ρ : E → K の例として，

θ(01, 1) = 0，θ(01, 2) = 01 である．整数 m = 3 にρ(e1 ) = 0, ρ(e2 ) = 1, ρ(e3 ) = 0 が存在する．

対しては，m > l である．よって，長さ m = 3 のト
レースは，θ(01, 3) = 010 である．

例 2 ここでも，例 1 のプログラムと二分木 T とを考える．今度は，定義 18 のガイド g として，ビット列

定義 15 に基づき，トレース s = 010 の定める

g = 001 ∈ S を与える．ガイド g に対する長さ 2 のト

比較構成の列 D(s)，および，s の定めるトレース

レース s は，s = θ(g, 2) = 00 である．g に対する長条件 Q(s) を考えていく．トレースの各ビットは，

さ 3 のトレース s′ は，s′ = θ(g, 3) = 001 である．両b1 = 0, b2 = 1, b3 = 0 である．定義 8 により，各プロ者の定めるトレース条件は，それぞれ，Q(s) = {e1 ≤グラム変数の初期の数式値 σ0 は，仕様変数によって，

e2 , e2 ≤ e3 }，Q(s′ ) = {e1 ≤ e2 , e2 ≤ e3 , e1 > e2 } とσ0 (x1 ) = e1 , σ0 (x2 ) = e2 , σ0 (x3 ) = e3 と表される．

なる．ここで，Q(s) は充足可能であるが，Q(s′ ) は

比較構成 (c1 , σ1 ; b1 ) を考える．最初の比較文は，

c1 = (x1 > x2 ) である．この比較文までにプログ充足不能である．定義 17 により，トレース s の切上
げ長は k = 3 である．

ラム変数の値は変更されない．よって，σ1 = σ0 で

ここで，定義 21 に従い，ガイド g に対する次のガイ

あ る ．比 較 構 成 の 真 偽 値 は b1 = 0 であ る ．定 義

ド g ′ を求める．トレース s については，長さ m = 3 と14 に基づき，この比較構成の定める比較命題を，切上げ長 k = 3 が同じである．g に対する長さ 3 の次

δ(c1 , σ1 ; b1 ) = (σ1 (x1 ) ≤ σ1 (x2 )) と得る．各変数ののガイド g ′ = ν(g, 3) を求めると，β(001) + 1 = 010

値 σ1 (x1 ) = σ0 (x1 ) = e1 ，σ1 (x2 ) = σ0 (x2 ) = e2 をだから，g ′ = 010 である．定義 24 で求める，ガイド

用いると，この不等式は e1 ≤ e2 となる．

g ′ に対する T の葉節点 v ′ は，g ′ に従ってプログラム

比較構成 (c2 , σ2 ; b2 ) を考える．前の比較構成により，次の比較文は，c2 = (x2 > x3 ) と定まる．この比較文を実行することで得られる．この場合の v ′ のラベル

λ(v ′ ) は，g ′ = 010 に等しい．

までにもプログラム変数の値は変更されない．よって，後の第 6 節で見るプログラムは，本節のバブルソー

σ2 = σ1 である．比較構成の真偽値は b2 = 1 である．

トと，それに後続する部分とから成る．このような場

定義 14 に基づき，この比較構成の定める比較命題を，合に，トレースの切上げ長を用いて次のガイドを求めδ(c2 , σ2 ; b2 ) = (σ2 (x2 ) > σ2 (x3 )) と得る．各変数のることで，不要なトレースを実行しないという効率化

値 σ2 (x2 ) = σ0 (x2 ) = e2 ，σ2 (x3 ) = σ0 (x3 ) = e3 をを行える．

用いると，この不等式は e2 > e3 となる．
比較構成 (c3 , σ3 ; b3 ) を考える．前の比較構成により，次の比較文は，c3 = (x1 > x2 ) と定まる．この比5 Scala に対するクラスライブラリ
5. 1 クラスライブラリの概観

較文までに，3 つの代入文 y := x2 , x2 := x3 , x3 := y

フレームワークの形式モデルに基いた，プログラムが存在する．よって，プログラム変数 x2 , x3 の値が，言語 Scala に対するクラスライブラリの構築についσ3 (x2 ) = σ2 (x3 )，σ3 (x3 ) = σ3 (y) = σ2 (x2 ) と変て述べる．ライブラリは，5 つのクラスから構成され更される．x1 の値は変更されず，σ3 (x1 ) = σ2 (x1 )る．これらのクラスの関係を，クラス名のみのクラスである．比較構成の真偽値は b3 = 0 である．定義

図 (図 3) に示す．本来，クラス図に書くべきフィール

14 に基づき，この比較構成の定める比較命題を，ドやメソッドは，クラスごとの表に示す．各表においδ(c3 , σ3 ; b3 ) = (σ3 (x1 ) ≤ σ3 (x2 )) と得る．各変数のて，最左の欄に Scala のプログラム断片を提示する．

値 σ3 (x1 ) = σ0 (x1 ) = e1 ，σ3 (x2 ) = σ0 (x3 ) = e3 を真中の欄に，それと対応する数学記法を示す．最も右の欄に，数学記法を導入した定義の番号を示す．

5. 2 数値変数クラス (表 1)
定義 5 のプログラム変数の集合 X と，数値変数./RQJ'RXEOH 6WDQGDUG ([SUHVVLRQ 6\PEROLF(Standard[K]) クラスとを対応付ける．定義 1 の数の 7UDFH ,QHTXDOLWLHV

集合 K と，型パラメータのクラス K とを対応付ける．
数値変数クラスは，クラス K のフィールド number を持つ．ここでは，K を Long 型と対応付ける．以降，クラス名に型パラメータ K を併記しないことがある．

図3

The Diagram of Class Names of the
Library

プログラム変数 x ∈ X が，数値 τ (x) = a ∈ Kを持つとする．変数 x を Standard クラスのインス
タンス x と，数 a を Long クラスのインスタンス a

5 つのクラスを順に挙げる．(1) 数値変数 (Standard)と，それぞれ対応付ける．このとき，数値 a を持つプ

クラス (表 1)，(2) 記号変数 (Symbolic) クラス (表ログラム変数 x は，コンストラクタの起動 x = new2)，(3) 数 式 (Expression) ク ラ ス (表 3)，(4) トStandard[Long](a) で構成され，x.number = a とレ ー ス (Trace) ク ラ ス (表 4)，(5) 線 形 不 等 式 系

なる．

(Inequalities) クラス，以上である．各クラスは，

集合 X 上の変数式の集合 K[X] について，定義 7

数値のプリミティブ型のクラス K を型パラメータとしで数値に関する算術演算，定義 13 で数値に関する比て取る．クラス K として，Long 型，または，Double

較演算を，それぞれ定義した．変数式 r ∈ K[X] も，型を用いる．記号変数クラスは，数値変数クラスのサ

数値変数クラスのインスタンスで表現する．各定義

ブクラスである．なお，線形不等式系クラスは，ソルで，集合 K[X] 上の演算を，集合 K 上の演算に帰着

バー Z3 との連携のためのクラスであり，形式モデル

した．数値変数クラスにおける演算は，K = Long 型との関連性が小さい．それで，このクラスに対する表の演算に帰着する．

は省略している．

変数式 p, q ∈ K[X] に対する加算 r = p + q を取り

定義 5 におけるプログラム変数 x ∈ X を，数値変上げる．変数式 p, q と，数値変数クラスのインスタン

数クラスと，記号変数クラスの両者のインスタンスで

ス p, q とをそれぞれ対応付けると，演算はメソッド表現する．プログラム変数 x ∈ X のインスタンスは，

起動 p + q と対応する．メソッドを起動するインスタ

数値変数クラスでは数値 τ (x) を持つ．記号変数クランス p を，内部から見て this とし，仮引数を同じ qスでは数値 τ (x) と数式値 σ(x) の両者を持つ．定義

で表す．また，演算結果の変数 r と，数値変数クラス

3 における数式 t ∈ K[E] を，数式クラスのインスタのインスタンス ret とを対応付け，これによりメソッンスで表現する．本節では，定義 15 におけるトレード内部での戻り値を表す．定義 7 より，変数式 r の持ス s として，定義 18 におけるトレース θ(g, m) を用

つ数値は，τ (r) = τ (p) + τ (q) である．メソッドでは，いる．ここに，g はガイド，m は s のトレース長であret.number = this.number + q.number とする．

る．トレース s = t(g, m) を，トレースクラスのイン

変数式 p, q ∈ K[X] に対する等価演算 p ≃ q を取スタンスで表現する．定義 15 における，トレース s

り上げる．これを，インスタンス p, q に対するメの定めるトレース条件 Q(s) を，線形不等式系クラス

ソッド起動 p.equals(q) と対応付ける．定義 13 にのインスタンスで表現する．

基づき，τ (p) ≃ τ (q) の真偽を決定する．メソッド内

数値変数クラスと，記号変数クラスとは，算術演算と比較演算のメソッド群を持つ．表 1，2 では，算術演算のメソッドは，加算 (add) メソッドで代表させ，比較演算のメソッドは，等価 (equals) メソッドで代表させる．

部では，Long クラス上の比較演算 this.number ==q.number を行い，Boolean 型の値を返す．

classStandard[K]

X

5

a∈K

1

fieldsnumber: K
constructor/construction
5Standard[K](number: K)
x = new Standard[Long](a)x∈X

5x.number = a

τ (x) = a ∈ K

5

add(q: Standard): Standard+

7

p.add(q)p+q7equals(that: Any): Boolean≃

13p.equals(q)

p≃q

13

method/invocation

表1

Standard class

5. 3 数式クラス (表 3)け，メソッドの引数に id を与える．数式クラス

クラスライブラリにおける主たるクラスは記号変の companion object のメソッドとする．

数クラスであるが，その説明のために，先に数式クラスとトレースクラスについて述べておく．

• メソッド + は，数式の加算 t = u + w(u, w ∈K[E]) を行う．数式 u, w と，数式クラスのイン

定義 2 の通り，仕様変数の集合を E = {e1 , · · · , en }スタンス u, w とをそれぞれ対応付けると，演算とする．定義 3 における E 上の数式の集合 K[E] と，はメソッド起動 u + w と対応する．u.coefs と数式 (Expression) クラスとを対応付ける．数式クラw.coefs の対応成分ごとの加算を，K = Long 型

スは，List[K] 型のフィールド coefs を持つ．

上で行う．

命題 1 により，数式 t ∈ K[E] は，定義 4 の正規• メソッド * は，数式の定数倍 t = a ∗ u(a ∈形 t = a0 + a1 ∗ e1 + · · · + an ∗ en で表すことがで

K, u ∈ K[E]) を行う．数式 u と数式クラスのイ

きる．いま，正規形の数式 t と，数式クラスのインス

ンスタンス u を対応付け，数 a と K = Long 型のタンス t とを対応付ける．t の係数列 (a0 , a1 , · · · , an )a とを対応付けると，演算はメソッド起動 u * aと，List[Long] のインスタンス list を対応付ける．

と対応する．u.coefs の各成分と a との乗算を，

ここで，ai (0 ≤ i ≤ n) と，list の第 i 成分とがK = Long 型上で行う．

対応する．このとき，数式 t はコンストラクタの起また，命題 2 に基づき，本クラスに数式のドット積

動 t = new Expression[Long](list) で構成され，のメソッドを設け，後述の記号変数の数式値の数値化

t.coefs = list となる．

に対応する．

命題 1 の各場合と対応するメソッドを，数式クラスに設ける．

5. 4 トレースクラス (表 4)• メソッド const は，t = a ∈ K に対応する数式

定義 18 におけるトレース s = θ(g, m) ∈ S を，トを生成する．整数 a と K = Long 型の a とを対レース (Trace) クラスのインスタンスで表現する，と応付け，メソッドの引数に a を与える．数式クラ述べた．トレースクラスのインスタンスは，記号変数

スの companion object のメソッドとする．

間の，トレース以外の共有情報も含む．共有情報は，• メソッド unit は，t = ek ∈ E に対応する数式(1) トレースに関するもの，(2) トレース条件に関すを生成する．添字 k と Int 型の id とを対応付るもの，(3) 記号変数のリストと成分数，以上に大別

classX

5number: Ka∈K

1

expression: Expressiont ∈ K[E]3

trace: Traces = θ(g, m)

18

id: Intn8

Symbolic[K] extends Standard[K]field

constructor/construction
5

Symbolic[K](expression: Expression, trace: Trace)x = new Symbolic[Long](t, trace)x∈X

5

x.expression = tσ(x) = t ∈ K[E]58

Symbolic[K](trace: Trace)x = new Symbolic[K](trace)xi ∈ P

8

x.expression = Expression.unit(trace.id)

σ0 (xi ) = ei ∈ K[E]8add(q: Standard): Standard+

6

p.add(q)p+q6equals(that: Any): Boolean≃

14p.equals(q)≃ (p, q)14

p.compare(q, c)▷◁ (p, q)14

instanciate()τ (x) = ρ(σ(x))

5

σ(xi ) = σ0 (xi )8method/invocation

initialize(i: Int)
表2

Symbolic class

される．

としている．Boolean 型のフィールド hasNextGuide(1) について，定義 18 におけるガイド g と，トレーは，次のガイドの存在を示す．メソッド nextGuide でスクラスのフィールド guide とを対応付ける．これは，次のガイドの長さ h として，トレース s = θ(g, m)

は，Int 型の ListBuffer である．また，ガイド g にのトレース長 m と，定義 17 のトレース s の桁上げ

対するトレース s のトレース長 m と，Int 型のフィー

長 k とを選択できる．トレースの切上げ長を選択す

ルド length とを対応付ける．定義に従い，これら 2ることを，Boolean 型のフィールド useFeasibility

つのフィールドを用いて，トレース s = θ(g, m) を表で表す．そして，トレースの桁上げ長 k と，Int 型

現する．トレースクラスのインスタンスを文字列化のフィールド cutLength とを対応付ける．また，ト(toString) すると，この s = θ(g, m) を表すビット

レース長の上限を Int 型のフィールド limitLength

列 (定義と同じ並び順) となる．

で表現する．

定義 21 で，ガイド g に対する長さ h の次のガイド(2) について，定義 15 における，トレース s の定ν(g, h) ∈ S を定義した．メソッド nextGuide は，現

めるトレース条件 Q(s) と，線形不等式系クラスの在のガイド guide に対する次のガイドを求め，guide

インスタンスのフィールド condition とを対応付けを更新する．なお，リスト guide の成分の並びは，こる．また，トレース条件 Q(s) の充足可能性と，Intのメソッドの実装を考慮して，定義のガイド g の逆順型のフィールド sat とを対応付ける．定義 16 におけclassExpession[K]

K[E]

3

(a0 , a1 , · · · , an )

4

field
coefs: List[K]constructor
4

Expession[K](coefs: List[K])method/invocation
add(w: Expression): Expression+

3

u.add(w)u+w

3

Expression.unit(id: Int): Expression
Expression.const(a: K): Expression
表3

Expession class

class
18

Trace[K]field
guide: ListBuffer[Int]g18length: Int

m

18
21

hasNextGuide: Boolean
cutLength: Int

k

17

Q(s)

15

limitLength: Int
condition: Inequalities

16

sat: Int
solution: Expression

ρ16

id: Intn8variables: List[Symbolic]P

8

constructor
18

Trace[K](numberType: Int)
methodν(g, h)nextGuide()
表4

る，トレース s に対する充足解 ρ と，線形式クラスのフィールド solution とを対応付ける．

(3) に つ い て ，定 義 8 に お け る 集 合 P

21

Trace class

い ま ，ト レ ー ス ク ラ ス の 新 規 の イ ン ス タ ン ス

trace を ，コ ン ス ト ラ ク タ の 起 動 trace = new=Trace[Long](0) で構成する．引数 0 は，ソルバー{x1 , · · · , xn } と ，記 号 変 数 ク ラ ス の イ ン ス タ ン ス

Z3 で整数型を用いることを意味する．コンストラクのリストのフィールド variables とを対応付ける．

タは，上記の各フィールドの初期化を行う．(1) につ

また，P の要素数 n と，Int 型のフィールド id とをいて，フィールド guide を空の ListBuffer とする．

対応付ける．

これは，定義 19 の初期ガイド g = ϵ を表現する．また，フィールド length を，整数 0 とする．

スのインスタンス x と対応付ける．同様に，インスタインスタンス trace の構成時には，次のガイド

ンス trace が生成されているとする．このとき，プとして初期ガイドが存在する．よって，フィールド

ログラム変数 xn は，コンストラクタの起動 x = newhasNextGuide を true とする．メソッド nextGuide

Symbolic[Long](trace) で構成される．

で 次 の ガ イ ド を 求 め る 際 ，そ の 長 さ は ，標 準 で

数式 en に対応する数式クラスのインスタンスは，は ト レ ー ス の 切 上 げ 長 と す る ．よって ，フィー ル

同クラスのメソッド unit で生成する．インスタンス

ド useFeasibility を true と す る ．フィー ル ド

trace はフィールド id を持ち，その値は整数 n−1 を表

cutLength は，length と同じ 0 とする．また，フィー

現している．コンストラクタは，unit を引数 trace.id

ルド limitLength を，整数 10 とする．

で起動し，戻り値をフィールド x.expression に収め(2) について，トレース条件のフィールド condition

る．整数 n − 1 を用いるのは，リストのインデックス

を，線形不等式系クラスの新規のインスタンスとすが 0 開始であることによる．その後，trace.id をイる．(3) について，集合 P のフィールド variables

ンクリメントし，trace.variables に this を追加

を新規のリストとし，P の要素数のフィールド id をする．なお，記号変数クラスのメソッド initialize

整数 0 とする．

により，インスタンスのフィールド expression を，

トレースクラスのメソッドについては，後で述べる．

構成時のものに初期化できる．

5. 5. 2 スーパークラスの数値フィールド
5. 5 記号変数クラス (表 2)

定 義 5 で ，プ ロ グ ラ ム 変 数 x ∈ X は ，数 式 値

定義 5 のプログラム変数の集合 X と，記号変数σ(x) ∈ K[E] と，数値 τ (x) = ρ(σ(x)) ∈ K とを持つ

(Symbolic) クラスとを対応付ける．記号変数クラスとした．記号変数クラスのメソッド instanciate は，は，数値変数クラスのサブクラスである．本クラス

数式値の数値化を行う．定義 16 のトレースに対するは，スーパークラスのフィールド number 以外に，数充足解 ρ と，トレースクラスのフィールド solution

式クラスのフィールド expression，トレースクラスとが対応する．メソッド instanciate は，プログラのフィールド trace，Int 型のフィールド id，以上

ム変数の数式値 expression と，トレース条件の充足を持つ．

解 trace.solution とを用いて，スーパークラスの5. 5. 1 インスタンスの構成

フィールド number に，プログラム変数の数値を設定

プログラム変数 x ∈ X が，数式値 σ(x) = t ∈ K[E]する．なお，記号変数クラスのインスタンスの構成時を持つとする．変数 x を Symbolic クラスのインスには，フィールド number に仮の値 0 を収める．

タンス x と，数式 t を Expression クラスのインスタ

プ ロ グ ラ ム 変 数 x と ，記 号 変 数 ク ラ ス の イ ン

ンス t と，それぞれ対応付ける．また，トレースク

ス タ ン ス x と を 対 応 付 け る ．変 数 x の 数 式 値 を

ラスのインスタンスとして，フィールド名と同名のσ(x) = a0 + a1 ∗ e1 + · · · + an ∗ en と す る と ，trace が生成されているとする．このとき，数式値 tx.expression のフィールド coefs は，σ(x) の係数を持つプログラム変数 x は，コンストラクタの起動

列 (a0 , a1 , · · · , an ) と対応する．命題 2 により，トx = new Symbolic[Long](t, trace) で構成され，レース条件の充足解 trace.solution のフィールド

x.expression = t となる．

coefs は，(1, ρ(e1 ), · · · , ρ(en )) と対応する．メソッ

定義 8 のプログラム変数 xi ∈ P ⊆ X については，

ド instanciate は，数式クラスのドット積のメソッ

生成時の数式値は既定である．そのため，特別なコンドを用いて，これらのベクトルのドット積を求め，戻ストラクタで構成する．いま，プログラム変数 xn をり値をフィールド x.number に収める．

構成し，集合 P = {x1 , · · · , xn−1 } に加えるとする．

5. 5. 3 算術演算

このとき，定義 8 により，xn は数式値 σ0 (xn ) とし

集合 X 上の変数式の集合 K[X] について，定義 6 でて，仕様変数 en を持つ．変数 xn を Symbolic クラ数式値に関する算術演算を定義した．変数式 r ∈ K[X]

も，記号変数クラスのインスタンスで表現する．定義<, !=のそれぞれに対して，0, 1, 2, 3, 4, 5 とす

で集合 K[X] 上の算術演算を，数式の集合 K[E] 上る．ここで，任意のメソッドに与える整数 c に対し，の演算に帰着した．記号変数クラスにおける算術演算

そのメソッドの否定の演算メソッドに与える整数をは，数式クラスにおける演算に帰着する．

5-c としている．

変数式 p, q ∈ K[X] に対する加算 r = p + q を取り

なお，equals メソッドについては，引数を that と上げる．変数式 p, q と，記号変数クラスのインスタして，クラスは任意 (Any) としている．that が数値

ンス p, q とをそれぞれ対応付けると，演算はメソッ

変数クラスのインスタンスでなければ，false を返ド起動 p + q と対応する．メソッドを起動するイン

す．that を数値変数に変換して q としたとき，q がスタンス p を，内部から見て this とし，仮引数を同

記号変数クラスのインスタンスでなければ，算術演算

じ q で表す．また，演算結果の変数 r と，記号変数の場合と同様に，同クラスへの変換を行う．

クラスのインスタンス ret とを対応付け，これによりメソッド内部での戻り値を表す．定義 6 より，変数

5. 6 比較演算メソッド compare

式 r の持つ数式値は，σ(r) = σ(p) + σ(q) である．メ

記号変数クラスの比較演算のメソッド compare に

ソッドでは，ret.expression = this.expression

ついて，詳細を述べる．ガイドに基づいてトレースを+ q.expression とする．

定め，比較構成のビットを得る．比較文と記号変数の

なお，引数 q のクラスは，数値変数クラスとしてい数式値を併せて比較命題を生成し，既存のトレース条

る．q が記号変数クラスのインスタンスでなければ，件に追加する．最後に，比較構成のビットを戻り値とそれは定数であるとみなし，同クラスへの変換を行して返す．

う．その場合，フィールド expression は，数式クラスのメソッド const を用いて設定する．

定義 18 に基づき，任意のビット列であるガイド

g = (b1 , · · · , bl ) ∈ S が与えられたとする．記号変

変数式の定数倍 r = a ∗ p は，2 つの変数式の乗算

数に関する比較演算が，プログラムの開始から数えとして実装している．メソッド * の引数の numberて j − 1 回行われたと仮定する．このとき，定義 18

フィールドを用い，数式クラスの定数倍の演算に帰着に基づき，g に対するトレース長 j − 1 のトレースしている．

s = θ(g, j − 1) ∈ S が定まる．すると，定義 15 に基5. 5. 4 比較演算

づき，トレース s が比較系列 D(s) と，トレース条件

変数式 p, q ∈ K[X] に対する等価演算 p ≃ q を取Q(s) とを定める．

り上げる．これを，インスタンス p, q に対するメ

ここで，メソッド compare で，j 回目の比較演算を

ソッド起動 p.equals(q) と対応付ける．同様に，メ行うとする．定義 14 に基づく，集合 X 上の比較文

ソッドを起動するインスタンス p を，内部から見て

cj = ▷◁ (p, q) と，写像 σj : X → K[E] が与えられた

this とし，仮引数を同じ q で表す．比較演算についてとする．定義 18 に基づき，g に対するトレース長 jは，σ(p), σ(q) の間，すなわち，this.expression,のトレース s′ = θ(g, j) を定め，その最後のビット bj

q.expession の間の大小関係は定義されない．そこを得る．集合 X 上の比較構成 (cj , σj ; bj ) は，比較命で，定義 14 に基づいて，比較命題の不等式を生成す

題 dj = δ(cj , σj ; bj ) を定める．定義 15 に基づき，トる．そのために，後述のメソッド compare を用いる．

レース s′ の定める比較構成列 D(s′ ) と，s′ の定める

このメソッドは，引数として，数値変数クラスの q，トレース条件 Q(s′ ) = Q(s) ∪ {dj } とを得る．

Int 型の c を取る．整数 c は，compare の呼び出し元

形式モデルでの上記の内容を，記号変数クラスの比較演算の種別を示す．メソッド equals の場合，cのメソッド compare の内容と対応付ける．比較文= 0 である．よって，メソッド起動 this.compare(q,cj = ▷◁ (p, q) における変数式 p, q と，記号変数クラ0) を行う．起動時の内容の詳細は後述する．

スのインスタンス p, q とをそれぞれ対応付ける．ま前記の整数 c は，メソッド equals, >=, <=, >,た，比較演算子 ▷◁ と，整数 c とを対応付ける．すると，比較演算はメソッド起動 p.compare(q, c) と対

makeInequality で行う．ビット bj が 1 ならば，応する．メソッドを起動するインスタンス p を，内部

メ ソッド 起 動 makeInequality(expression,から見て this とし，仮引数を同じ q で表す．以下，

q.expression, c) を行う．ビット bj が 0 ならば，インスタンス this のフィールド this.trace を，単メ ソッド 起 動 makeInequality(expression,に trace と記す．起動されたメソッド内部では，次q.expression, 5-c) を行う．
• トレース条件 Q(s′ ) = Q(s) ∪ {dj } に対し，そを順次行う．

• 定義 18 に基づき，ガイド g に対するトレースの充足可能性を調べる．更新されたフィールド

長 j のトレース s′ = θ(g, j) を求める．ガイド

condition に対し，線形不等式系クラスのメソッは，trace のフィールド guide で，トレース長

ド solve を起動する．メソッドの戻り値が充足

は，trace のフィールド length で，それぞれ表可能性を示すので，これをフィールド sat に収現する．まず，トレース長を j にする．すなわ

める．充足可能ならば sat は 1 となり，充足不ち，length をインクリメントする．

能ならば sat は 0 となる．

次に，比較構成におけるビット bj を決定する．ト• トレース条件 Q(s′ ) が充足可能であるとする．

レース長 j がガイド g の長さ以下 (j ≤ l) の場合，

定義 16 の s′ に対する充足解 ρ は，condition

トレース θ(g, j) はガイド g の部分列 (b1 , · · · , bj )のフィールド solution に収められる．そこで，である．フィールド guide は逆順で実装していtrace のフィールド solution にもそれを参照さるため，bj は guide の第 guide.size - length

せる．なお，現在の実装では，ここでの，記号変成分である．

数の数式値の充足解による数値化はしていない．

トレース長 j がガイド g の長さを超える (j > l)

• トレース条件 Q(s′ ) が充足不能であるとする．ト場合，トレース θ(g, j) は，トレース θ(g, j − 1)

レース条件 Q(s) が充足可能であった場合は，定にビット bj = 0 を追加したものである．この場

義 17 に基づき，トレース s′ の切上げ長 k を定め

合，guide の先頭に，整数 0 を追加する．guideる．整数 k と，trace のフィールド cutLengthの先頭は，やはり第 guide.size - length 成分が対応する．trace の構成時の cutLength の値である．

は 0 である．トレース条件が充足可能であり続• 定義 14 に基づき，比較構成 (cj , σj ; bj ) から，比較

ける限り，cutLength の値は 0 のまま変更しな

命題 dj = δ(cj , σj ; bj ) を定める．そして，トレーい．現在の cutLength の値が 0 であれば，Q(s)′′ス s の定めるトレース条件 Q(s ) = Q(s) ∪ {dj }は充足可能である．ここで，cutLength の値を，を得る．比較命題 dj は次の通りである．

トレース s′ の長さ，すなわち，length とする．

– bj = 1 ならば，dj = ▷◁ (σj (p), σj (q))．

• 戻り値を返してメソッド compare を終了する．

– bj = 0 ならば，dj = ¬ ▷◁ (σj (p), σj (q))．

ビット bj ，すなわち，guide の guide.size -

ここで，数式 σj (p), σj (q) ∈ K[E] と，インスタ

length 成分が 0 ならば false を，1 ならば true

ンス this, q のフィールド this.expression,を返す．

q.expression とが，それぞれ対応する．また，比較演算子 ▷◁, ¬ ▷◁ と，整数 c, 5-c とがそれぞ5. 7 次のガイドを求めるメソッド nextGuide

れ対応する．

定義 21 において，ガイド g ∈ S と整数 h とがト レ ー ス 条 件 Q(s) と ，trace の フィー ル ド

与えられたときの，g に対する長さ h の次のガイ

condition とが対応する．このフィールドは，

ド ν(g, h) ∈ S を定めた．トレースクラスのメソッ

後述の線形不等式系クラスのインスタンスであド nextGuide は，同クラスのインスタンス trace のる．比較命題 dj の生成と，それのトレース条件

フィールド guide を，次のガイドを表現するものにQ(s) への追加は，線形不等式系クラスのメソッド更新する．さらに，guide 以外の各フィールドを初期

化して，次のガイドによる記号実行の準備を行う．以ラスのインスタンスである．トレース条件の充足可能下で，メソッド nextGuide で行う操作を述べる．

性判定には，ソルバー Z3 [21] を用いる．Z3 は Java• ガ イ ド guide の 長 さ が ト レ ー ス 長 の 上 限
limitLength を超えている場合，guide の長さ

API を提供するので，JVM 上で動作する Scala プ
ログラムで用いることができる．

が limitLength になるまで，その成分を削除す

本クラスのフィールドのうちの 3 つは，Z3 のクラる．先述の通り，リスト guide の成分の並びは，

スを使用している．Context クラスのインスタンス

モデルにおける並びの逆順となっている．よっのフィールド context, Solver クラスのインスタンて，リストの先頭から順に成分を削除する．

スのフィールド solver，ArithExpr クラスのインス• 次 の ガ イ ド の 長 さ と し て ，ト レ ー ス の 切 上

タンスのリスト variables，以上である．variables

げ 長 cutLength を 選 択 す る 場 合 ，次 を 行 う．

は仕様変数のリストを表現する．さらに，トレース条

cutLength の値が 1 以上であれば，記号変数

件の充足解を表現する，Expression クラスのフィークラスのメソッド compare で，トレースの切上

ルド solution を持つ．

げ長が設定されたことを意味する．この場合，

本クラスの新規のインスタンスは，コンストラクタ

guide の長さが cutLength になるまで，その成の起動 condition = new Inequalities[Long](0)分を削除する．ここで，cutLength を 0 に初期で構成される．ここで，引数 0 は，Z3 で整数型を用化する．

いることを意味する．以下，この仮定の下で説明を行• 定義 21 に基づき，guide を次のガイドに更新
する．ビット列 θ(g, h) は，現在の guide と対う．実数型を用いる場合の引数は 1 であるが，説明は省略する．

応する．2 進数 β(θ(g, h)) に 1 を加える操作を，

コンストラクタでは，まず，フィールド context

guide に対して行う．guide の先頭の成分から順を ，Context ク ラ ス の 新 規 イ ン ス タ ン ス と す る ．

に，値を調べる．1 であればそれを取り除いて，

次に，フィールド solver を，context がメソッド

次の成分を調べる．0 であればそれを 1 に変更し

mkSolver を起動した戻り値とする．そして，フィーて，この操作を終了する．この操作で，全てのルド variables を，新規のリストとする．

成分が 1 と判明すれば，次のガイドは存在しな

本クラスは，2 つのメソッドを持つ．線形不等式

い．この場合，次のガイドの存在 hasNextGuide

系への不等式の追加を行うメソッド makeInequality

を false にする．

と，線形不等式系の充足可能性判定を行うメソッド• トレース長 length を 0 に初期化する．
• トレース条件 condition を，線形不等式系クラスの新規のインスタンスとする．
トレースクラスには，他にも次の各メソッドを設ける．メソッド instanciate は，フィールド variables

solve である．
記号変数クラスのメソッド compare において，本クラスのメソッド makeInequality を起動した．メ
ソッド makeInequality(u, w, c) の内部では，次を順次行う．

の成分の各記号変数に対して，記号変数クラスの• 不等式の左辺の数式 u から右辺の数式 w を引き，

instanciate を適用する．メソッド initialize は，

数式クラスのインスタンス t とする．いま，t が，各記号変数に対して，記号変数クラスの initialize

定義 4 の正規形の数式 a0 + a1 ∗ e1 + · · · + an ∗ enを適用する．

を表現しているとする．

• フィールド variables は，ソルバーで用いる変5. 8 線形不等式系クラス

数のリストである．仕様変数 ei (1 ≤ i ≤ n) と，

定義 15 のトレース条件 Q(s) を，線形不等式系

variables の第 i-1 成分とを対応付ける．数式 t(Inequalities) クラスのインスタンスで表現する．

のフィールド coefs の長さが variables の長さ

トレースクラスのフィールド condition が，このクより長い場合，新規の変数を variables に追加す

る．これは，context の，メソッド mkIntConst

6 不完全なバブルソートの例題の起動により行う．

• 数式 t を，Z3 の ArithExpr クラスのインスタ

本節では，Scala プログラムの例題を取り上げ，フンス zt に変換する．最初に，zt を，t の定数項

レームワークを用いた記号実行によるテストについて

a0 を表現する式にする．a0 と，t.coefs の第 0説明する．次のプログラム中の 2 つのメソッド typeA,成分とが対応する．これは，context の，メソッ

typeB の等価性のテストを行う．

ド mkInt の起動により行う．

package test

• 次に，zt に，t の各仕様変数 ei と係数 ai の積を追加していく．ai と，t.coefs の第 i 成分とが対応し，ei と，variables の第 i-1 成分とが対応

import es._class Triangle (var x1: Standard[Long], var x2:
Standard[Long], var x3: Standard[Long]) {する．積 ai ∗ ei は，context の，メソッド mkMul

def typeA() : Int = {の起動により求める．zt への加算は，context

if (x1 + x2 > x3 && x2 + x3 > x1 && x3 + x1
> x2) {
if (x1 == x2 && x2 == x3) {3} else if (x1 == x2 || x2 == x3 || x3 ==x1) {2} else {1}} else {0}の，メソッド mkAdd の起動により行う．

• 左辺を zt，右辺を 0 とする不等式を作成する．
これは，context の，比較演算のメソッドを起動により行う．引数を zt，および，定数 0 とす
る．比較演算には，mkEq, mkGe, mkLe, mkGt,

mkLt の 5 種類がある．メソッド makeInequalityの引数 c に応じて，上記のいずれかを選択する．

c の値が 5(比較演算子 ̸≃) の場合，mkGt, mkLt}

による不等式を，論理演算のメソッド mkOr で

def typeB(): Int = {結ぶ．

var y = new Standard[Long](0)if (x1 > x2) {y = x1x1 = x2
x2 = y}if (x2 > x3) {y = x2x2 = x3
x3 = y}if (x1 > x2) {y = x1x1 = x2
x2 = y}if (x1 + x2 > x3){
if (x1 == x2) {if (x2 == x3) 3
else 2} else {if (x2 == x3) 2
else 1}} else {0}• フィールド solver のメソッド add の起動により，solver に上記の不等式を追加する．
メソッド solve では，線形不等式系クラスのインス
タンスに対する充足可能性判定を，フィールド solverのメソッド check の起動により行う．このメソッドの戻り値が充足可能性を示す．充足可能な場合のモデ
ルは，solver のメソッド getModel の起動により得る．得られたモデルのインスタンスを model とする．
例えば，model の evaluate メソッドの起動により，variables の各変数の値を得ることができる．ここでは，evaluate メソッドの戻り値を文字列で得て，それを整数に変換している．実数型の場合，有理数が，分子と分母がスラッシュで区切られた文字列として得られるので，これをもとに実数に変換する．各変数の値をもとに，数式クラスのフィールド solutionを構成する．命題 2 に基づき，solution.coefs は，第 0 成分を 1 とし，第 i 成分を仕様変数 ei の値 ρ(ei )
とする．

}
}

プログラムは，Myers の三角形問題 [12] に基づいている．この問題におけるプログラムは，3 つの整数値を入力したとき，それらを長さとする三辺で構成されimport scala.collection.mutable._
import org.junit._
import Assert._
import es._

る，三角形の種別を出力するものである．ここでは，三角形の種別を整数で表す．正三角形に整数 3，二等辺三角形に整数 2，不等辺三角形に整数 1 をそれぞれclass TestTriangle {@Test
def testStandard {与える．3 つの整数で三角形が構成されない場合，整var x1 = new Standard[Long](2)var x2 = new Standard[Long](2)var x3 = new Standard[Long](1)val tri = new Triangle(x1, x2, x3)
val typeA = tri.typeA()val typeB = tri.typeB()
assertEquals(typeA, typeB)

数 0 を与える．

Myers は，三角形問題に対するテストケースとして選択すべきものをいくつか挙げている [12]．その中に「二等辺三角形の場合に，3 辺の 3 種類の組合せを全て網羅せよ，例えば (3, 3, 4), (3, 4, 3), (4, 3, 3)．
」というものがある．Myers の指摘は妥当であるのだが，}@Test
def testSymbolic {ここで挙げている例は等辺が最小辺となる場合である．等辺が最大辺，かつ，2 種類の組合せしか網羅しない場合に，検出できない欠陥を含むプログラムが存在するので，それを示す．これは，提案するフレーム
ワークに限らない，記号実行によるテストの有効性を示す例である．
プログラム中の 2 メソッド typeA, typeB は，上記の仕様を満たすように実装したものである．メソッ
ド typeA は，三角不等式 x1 + x2 > x3 ∧ x2 + x3 >x1 ∧ x3 + x1 > x2 を用い，仕様を忠実に実装したものである．メソッド typeB は，三角不等式の一つの十分条件 x1 ≤ x2 ≤ x3 ∧ x1 + x2 > x3 をもとに実装したものである．三数 x1 , x2 , x3 を x1 ≤ x2 ≤ x3 を満たすようにソーティングして，三辺の長さの間の不等式を一つとしたものである．ここで，第 4 節で例題とした，バブルソートを用いている．2 つのメソッドで，三角形が構成される場合の種別の判定の部分が異なっている．メソッド typeB のその部分は，性質

x1 ≤ x2 ≤ x3 に依存している．
2 節で述べた，本フレームワークの使用法に従って，対象プログラム，および，テストプログラムを説明する．対象プログラムのフィールド x1, x2, x3
は，本来のプリミティブの Long 型から，数値変数

Standard[Long] 型に改編されている．また，この改編の影響により，メソッド typeB の局所変数 y も型の変更を受けている．
package test

val trace = new Trace[Long](0)var x1 = new Symbolic[Long](trace)
var x2 = new Symbolic[Long](trace)
var x3 = new Symbolic[Long](trace)
trace.limitLength = 20// trace.useFeasibility = false// trace.guide = ListBuffer[Int](0,0,1,1,0,1,0,1,1,1,1)
var count = 0
while (trace.hasNextGuide) {println("*"+count)
val tri = new Triangle(x1, x2, x3)
val typeA = tri.typeA()val typeB = tri.typeB()
println(trace)
if (trace.sat == 1){
assertEquals(trace.solution.toString(),
typeA, typeB)}
count += 1
trace.nextGuide()}}}

テストプログラムの説明を行う．等価性のテストには，フレームワーク JUnit [9] を用いる．Scala プロ
グラムは JVM 上で動作するので，JUnit を利用できる．テストプログラム中の前者のメソッドでは，数値変数を用いて対象の Triangle クラスのインスタン
スを構成し，後者のメソッドでは，記号変数を用いてインスタンスを構成している．
以下，後者について説明する．テスト対象のメソッ
ド typeA, typeB を順次起動しているが，本来は，

typeB の起動前に，記号変数の数式値の初期化が必要である．これを省略しているのは，typeA では変数値

が変化しないためである．経路条件が充足可能な場

このフィールドの値を変更している．

合に，アサーションで，typeA と typeB の戻り値のな お ，以 上 の 各 テ ス ト は ，次 の 環 境 で 実 行 し一致を調べている．JUnit のメソッド assertEquals

た．Scala 2.11.8, Z3-4.4.1, JUnit 4.12, JavaSE-1.7,の第 1 引数で，経路条件の充足解の表示を指示してScala-IDE 4.4.1, Eclipse 4.5, Windows 7 SP1 64bit,

いる．

Core i7-4770 3.4GHz, 8GB RAM.

さて，後者のテストメソッドを用いて，次の 2 つのテストを行う．(1) メソッド typeA, typeB を記述し7 まとめと今後の課題

た通りのものとし，両者の等価性をテストする．(2)

本論文では，プログラム言語の標準解釈系上での記メソッド typeB のバブルソートにおいて，3 度目の大号実行のための，一つのフレームワークを提案した．

小比較と変数値の交換を省略する変更を行う．テスト

また，プログラム言語 Scala に対するフレームワー

により，欠陥を検出する．

クのクラスライブラリについて述べた．ライブラリの(1) のテストは 73 個のトレースを実行し，成功する．

規模の小ささも示している．また，例題プログラムにテストの実行時間は約 0.6 秒である．(2) のテストは対して，単体テストのためのフレームワークを標準解44 個のトレースを実行した後，失敗する．テストの実釈系上で併用し，記号実行による網羅的なテストを

行時間は約 0.4 秒である．JUnit の failure trace は，行った．

アサーションの反例 ρ(e1 ) = 2, ρ(e2 ) = 2, ρ(e3 ) = 1

本論文で提案するフレームワークの有効性についを出力する．ここで，e1 , e2 , e3 は，x1 , x2 , x3 のそれぞては，今後の研究によって実証しなければならない．

れに対する仕様変数である．実際には，failure trace

以下，第 2 節の「本フレームワークの適用範囲」，「ク

は，命題 2 のベクトル (1, ρ(e1 ), ρ(e2 ), ρ(e3 )) を示す．

ラスライブラリの使用法」を承けて，今後の課題や注反例の示す三角形は二等辺三角形なので，正しいメ

意すべき事項について述べる．

ソッド typeA は 2 を返すが，誤ったメソッド typeB• 演算子多重定義の機能を持たないオブジェクト

は 1 を返す．数値変数を用いたテストメソッドは，こ指向言語の対象化を考える．例えば，Java はこの反例に基づいて作成したものであり，同様にテストの機能を持たない．この場合，記号変数上の比は失敗する．

較演算や算術演算を，greaterThan や add など

こ の テ ス ト で は ，ト レ ー ス ク ラ ス の メ ソッドのメソッド名によって定義しなければならない．

nextGuide は，次のガイドの長さとして，標準の，記号実行の対象のプログラム中にプリミティブ

トレースの切上げ長を選択している．次のガイドの変数上の演算子 > や + による演算が存在すると長さとしてトレース長を用いた場合，(1) のテスト

き，プリミティブ変数を数値変数に置き換えるだは 480 個のトレースを，約 2.9 秒で実行する．(2) のけでなく，演算を定義したメソッドによるものにテストは 207 個のトレースを，約 1.3 秒で実行する．

書き換える必要がある．

この例題では，定義 24 で葉節点の巡回手続きを与え

このような言語を対象とする場合には，トランス

た，二分木の大きさは計算できる．メソッド typeA,

レータの開発も，有効な手段となり得る．対象のtypeB について，二分木の葉節点の数は，それぞれクラスを，記号実行用の別のクラスに変換するの

12, 40 である．両者を順次実行した場合，二分木のである．しかし，トランスレータで構文解析が必

葉節点の数は 480 である．(1) のテストの結果は，全要になれば，記号実行用の特別な解釈系に近いもての葉節点が巡回されていることを示している．まのとなってしまう．

た，typeA, typeB について，二分木の高さはそれぞ• オブジェクト指向でないプログラム言語の対象

れ 8, 6 である．両者を順次実行した場合の高さは 14化を考える．例えば，C 言語でオブジェクト指であり，トレースクラスの比較文の数の上限のフィー向プログラムを記述するためのフレームワーク

ルド limitLength の標準値 10 を超える．そのため，(名称は C+) が存在する [15]．このフレームワー

クは，オブジェクト指向の主要原理である，抽るのである．これは，記号変数の数式値の履歴

象化 (abstraction)，継承 (inheritance)，多相性を残さないという方針に基づいている．例えば，(polymorphism) を，C 言語におけるメタパター

数式値の履歴を，トレースクラスのフィールドでンとして実装したものである．このようなフレー

保存すれば，本フレームワークでもバックトラッ

ムワークを用いれば，非オブジェクト指向言語にクを行うことができる．

対しても，本論文のアプローチを適用できる可能性がある．

• 本フレームワークでは，対象のプログラムを，数値のプリミティブ型ではなく，数値変数クラスを• 記号実行の対象の算術演算の，四則演算への拡用いて記述する必要がある．同一の算術演算を，張を考える．この場合，記号変数の数式値は，有数値変数クラスによるプログラムと，プリミティ

理式になる．数式クラスを有理式のクラスとする

ブ型によるプログラムとで実行し，実行時間を計ことは難しくない．単項式，多項式，有理式の各測する簡単な実験を行った．その結果，前者の時

クラスを順に実装すればよい．問題となるのは，間の後者の時間に対する比は，1.1 以下である．

不等式系の充足可能性判定である．有理式に関す• 先 述 の 比 較 文 の 数 の 上 限 の フィー ル ド

る不等式は，分母を払って，多項式に関する不等limitLength を 設 け て い る 真 の 理 由 は ，比 較

式 (高次不等式) に変形できる．今後，ソルバー

文がループの終了条件に記述された場合に対応

Z3 の高次不等式への対応 [8] について調べ，このするためである．ループの終了条件の比較文が記拡張に取り組む予定である．

号変数を含む場合，記号実行は無限ループとな• 記号実行の実行効率は重要な論点である．しかる．現在の本フレームワークは，ループ不変条件

し，既存のアプローチとの効率面での比較は，今の自動生成 [11] [14] [16] を取り扱うものではない．

回の論文では取り扱わなかった．本フレームワー

なお，アサーションとしてループ不変条件を記述

クを単独で評価すれば，実行効率は実用的と判断し，これが比較文の数の上限までの範囲で満たさする．クラスライブラリのトレースクラスにおれるかどうかのテストは，現状でも可能である．

いて，比較文の数の上限 limitLength の標準値
を 10 としている．この値は，単体テストにおけ

参 考 文 献る，テスト対象のメソッドに現れる比較文の数を[ 1 ] Anand, S., Păsăreanu, C.S. and Visser, W.:
JPF-SE: a symbolic execution extension to Java
PathFinder, Proc. of the International Conferenceon Tools and Algorithms for the Construction andAnalysis of Systems (TACAS 2007), 2007, pp.134138.
[ 2 ] Apt, K.R.: Ten Years of Hoare’s Logic: A Survey - Part I, ACM Transactions on Programming
Languages and Systems, Vol.3, No.4, 1981, pp.431–
483.
[ 3 ] Binder, R.: Testing Object-Oriented Systems:
Models, Patterns, and Tools, Addison-Wesley, 2000.
[ 4 ] Cadar, C. et al.: Symbolic Execution for Software Testing in Practice Preliminary Assessment,
Proc. of the 33rd International Conference on Software Engineering (ICSE 2011), 2011, pp.1066–1071.
[ 5 ] Cadar C. and Sen K.: Symbolic execution for
Software Testing: Three Decades Later, Communications of the ACM, Vol.56, No. 2, 2013, pp.82–90.
[ 6 ] Dutertre, B. and de Moura, L.: A Fast LinearArithmetic Solver for DPLL(T), Proc. of the International Conference on Computer-Aided Verification (CAV 2006), LNCS, Vol.4144, Springer-Verlag,

想定したものである．この下で，葉節点の巡回手
続きの対象の二分木の節点数は，高々210 個，すなわち 1000 個程度である．第 6 節の例題に対する実行時間を参考にすれば，この規模の問題のテストの実行時間は数秒程度と言える．よって，十分に実用的であると結論する．

• 本フレームワークの効率化のための方法として，
例えば以下が存在する．記号実行に対する既存のアプローチでは，経路の網羅を行う際に，経路のバックトラックを行うものがある [1]．本フ
レームワークでは，比較文ごとの充足可能性判
定は行っている．しかし，次のガイドを求めるメ
ソッド nextGuide 中で，トレース長のフィール
ド length を 0 に初期化している．すなわち，次のガイドに従って，プログラムを最初から実行す2006, pp.81–94.
[ 7 ] 林晋: プログラム検証論, 共立出版, 1995.
[ 8 ] Jovanovic, D. and de Moura, L.: Solving
Non-Linear Arithmetic, Proc. of the International
Joint Conference on Automated Reasoning (IJCAR 2012), LNCS, Vol.7364, Springer-Verlag, 2012,
pp.339–354.
[ 9 ] JUnit, http://junit.org/[10] King, J.C.: Symbolic Execution and Program
Testing, Communications of the ACM, Vol.19, No.7,
1976, pp.385-394.
[11] Kovacs, L.: A Complete Invariant Generation
Approach for P-solvable Loops, Proc. of the 7thInternational Andrei Ershov Memorial Conference
on Perspectives of Systems Informatics (PSI 2009),
2009, pp.242–256.
[12] Myers, G.J.: The Art of Software Testing, 1stEdition, John Wiley & Sons, 1979.
[13] Păsăreanu, C., Mehlitz, P., Bushnell, D.,
Gundy-Burlet, K., Lowry, M., Person, S. and Pape,
M.: Combining Unit-Level Symbolic Execution and
System-Level Concrete Execution for Testing NASA
Software, Proc. of the ACM/SIGSOFT International Symposium on Software Testing and Analysis(ISSTA 2008), 2008, pp.15–26.
[14] Rodriguez-Carbonell, E. and Kapur, D.: Generating All Polynomial Invariants in Simple Loops,
Journal of Symbolic Computation, Vol.42, No.4,
2007, pp.443-476.
[15] Samek, M.: Practical Statecharts in C/C++,CMP Books, 2002.
[16] Sankaranarayanan, S., Sipma, H.B. and Manna,Z.: Non-linear Loop Invariant Generation using Groebner Bases, Proc. of 31st Annual ACM
SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages (POPL 2004), 2004,
pp.318-329.
[17] Smans, J., Jacobs, B. and Piessens, F.: HeapDependent Expressions in Separation Logic, Proc.
of FMOODS/FORTE 2010, LNCS, Vol.6117, 2010,
pp.170-185.
[18] 玉井 哲雄, 三嶋 良武, 松田 茂広: “ソフトウェアのテスト技法”, 共立出版, 1988.
[19] Visser, W., Havelund, K., Brat, G., Park, S. andLerda, F.: Model Checking Programs, AutomatedSoftware Engineering Journal, Vol.10, No.2, 2003.
[20] The Yices SMT solver, http://yices.csl.sri.com/[21] The Z3 Theorem Prover,
https://github.com/Z3Prover/z3/wiki

たものである．
以下に，クラスライブラリ Es[Scala] のソースコー
ド (Version 1.0) を示す．

A. 1 ライセンス条項
Es[Scala] is free software: you can redistribute
it and/or modify it under the terms of the
GNU General Public License as published by
the Free Software Foundation, either
version 3 of the License, or (at youroption) any later version.
Es[Scala] is distributed in the hope that it
will be useful, but WITHOUT ANY WARRANTY;
without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULARPURPOSE. See the GNU General Public
License for more details.
You should have received a copy of the GNU
General Public License along with Es[Scala]. If not, see <http://www.gnu.org/licenses/>.

A. 2 数値変数クラス
package es/*** This class is part of Es[Scala]* Copyright (c) 2016 Satoshi Hattori*/class Standard[K] (var number: K) (implicit num:
Numeric[K]) {override def toString(): String = {number.toString}
override def equals(that: Any): Boolean = {if (!that.isInstanceOf[Standard[K]]) {false} else {val q = that.asInstanceOf[Standard[K]]if (number == q.number) {true} else {false}}

A クラスライブラリのソースコード}

本論文で提案するフレームワークの名称は，Es[L](エdef >=(q: Standard[K]): Boolean = {ス・エル) とする．Es は，Execute symbolically に由

num.gteq(number, q.number)

来する．L は言語パラメータであり，Es[L] は Scala}

において型パラメータを取るクラス名の構文をまね

def <=(q: Standard[K]): Boolean = {num.lteq(number, q.number)}def compare(q: Symbolic[K], c: Int): Boolean ={var ret = false
trace.length += 1
if (trace.length > trace.guide.size) {trace.guide.insert(0, 0)}
if (trace.guide(trace.guide.size - trace.
length) == 0) {trace.condition.makeInequality(expression,
q.expression, 5 - c)
} else {trace.condition.makeInequality(expression,
q.expression, c)
ret = true}
trace.sat = trace.condition.solve()if (trace.sat == 1) {trace.solution = trace.condition.solution}
if (trace.sat == 0 && trace.cutLength == 0){
trace.cutLength = trace.length}
retdef >(q: Standard[K]): Boolean = {num.gt(number, q.number)}def <(q: Standard[K]): Boolean = {num.lt(number, q.number)}
def !=(q: Standard[K]): Boolean = {num.gt(number, q.number) || num.lt(number, q.number)}
def +(q: Standard[K]): Standard[K] = {new Standard[K](num.plus(number, q.number))}def -(q: Standard[K]): Standard[K] = {new Standard[K](num.minus(number, q.number))}}override def equals(that: Any): Boolean = {def *(q: Standard[K]): Standard[K] = {if (!that.isInstanceOf[Standard[K]]) {false} else {val q = that.asInstanceOf[Standard[K]]if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)compare(new Symbolic[K](w, trace), 0)
false} else {compare(q.asInstanceOf[Symbolic[K]], 0)}}

new Standard[K](num.times(number, q.number))}}A. 3 記号変数クラス
package es/*** This class is part of Es[Scala]* Copyright (c) 2016 Satoshi Hattori*/}
override def >=(q: Standard[K]): Boolean = {if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)compare(new Symbolic[K](w, trace), 1)} else {compare(q.asInstanceOf[Symbolic[K]], 1)}

class Symbolic[K] (var expression: Expression[K], val trace: Trace[K])(implicit num: Numeric[K]) extends Standard[K](num.zero) {var id = -1}
def this(trace: Trace[K]) (implicit num:
Numeric[K]) = {override def <=(q: Standard[K]): Boolean = {if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)compare(new Symbolic[K](w, trace), 2)} else {compare(q.asInstanceOf[Symbolic[K]], 2)}this(Expression.unit(trace.id), trace)
id = trace.id
trace.id += 1
trace.variables :+= this}override def toString(): String = {"[" + id + "]" + expression + "(" + number +")"}}override def >(q: Standard[K]): Boolean = {if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)compare(new Symbolic[K](w, trace), 3)} else {compare(q.asInstanceOf[Symbolic[K]], 3)}

expression = Expression.unit(id)}}}override def <(q: Standard[K]): Boolean = {if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)compare(new Symbolic[K](w, trace), 4)} else {compare(q.asInstanceOf[Symbolic[K]], 4)}

A. 4 数式クラス
package es/*** This class is part of Es[Scala]* Copyright (c) 2016 Satoshi Hattori*/}
override def !=(q: Standard[K]): Boolean = {class Expression[K] (val coefs: List[K]) (implicit num: Numeric[K]) {if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)compare(new Symbolic[K](w, trace), 5)} else {compare(q.asInstanceOf[Symbolic[K]], 5)}

override def toString(): String = {coefs.toString}
def +(w: Expression[K]): Expression[K] = {}var list = List[K]()for (i <- 0 until coefs.size)
if (i < w.coefs.size)
list :+= num.plus(coefs(i), w.coefs(i))
elselist :+= coefs(i)for (i <- coefs.size until w.coefs.size)
list :+= w.coefs(i)new Expression[K](list)

override def +(q: Standard[K]): Symbolic[K] ={if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)
new Symbolic[K](expression + w, trace)} else {val w = q.asInstanceOf[Symbolic[K]].
expression
new Symbolic[K](expression + w, trace)}}
def -(w: Expression[K]): Expression[K] = {}var list = List[K]()for (i <- 0 until coefs.size)
if (i < w.coefs.size)
list :+= num.minus(coefs(i), w.coefs(i))
elselist :+= coefs(i)for (i <- coefs.size until w.coefs.size)
list :+= num.negate(w.coefs(i))
new Expression[K](list)

override def -(q: Standard[K]): Symbolic[K] ={if (!q.isInstanceOf[Symbolic[K]]) {val w = Expression.const(q.number)
new Symbolic[K](expression - w , trace)} else {val w = q.asInstanceOf[Symbolic[K]].
expression
new Symbolic[K](expression - w, trace)}}
def *(a: K): Expression[K] = {}var list = List[K]()for (i <- 0 until coefs.size)
list :+= num.times(coefs(i), a)
new Expression[K](list)

override def *(q: Standard[K]): Symbolic[K] ={new Symbolic[K](expression * q.number, trace)}}

def *(w: Expression[K]): K = {def instanciate() = {var ret = num.zero
for (i <- 0 until coefs.size)
if (i < w.coefs.size)
ret = num.plus(ret, num.times(coefs(i),w.coefs(i)))
retnumber = expression * trace.solution}
def initialize(i: Int) = {}number = num.zero
id = i}guide.remove(0)if (!useFeasibility)
cutLength = 0
if (cutLength > 0 && guide.size > cutLength){
for (i <- 0 until guide.size - cutLength)
guide.remove(0)cutLength = 0}
while (!next && guide.size > 0) {if (guide(0) == 1) {val before = guide.size
guide.remove(0)if (before > guide.size || guide.size== 0)
first = false} else {guide(0) = 1
next = true}}
hasNextGuide = next || firstlength = 0
condition = new Inequalities(numberType)object Expression {def const[K](a: K) (implicit num: Numeric[K]):Expression[K] = {var list = List[K]()list :+= a
new Expression[K](list)}
def unit[K](id: Int) (implicit num: Numeric[K]): Expression[K] = {var list = List[K]()list :+= num.zero
for (i <- 0 until id)
list :+= num.zero
list :+= num.one
new Expression[K](list)}}}

A. 5 トレースクラス

def instanciate() = {package esfor (i <- 0 until id)
variables(i).instanciate()

import scala.collection.mutable._}/*** This class is part of Es[Scala]* Copyright (c) 2016 Satoshi Hattori*/

def initialize() = {for (i <- 0 until id)
variables(i).initialize(i)class Trace[K] (val numberType: Int) (implicit
num: Numeric[K]) {}}var guide: ListBuffer[Int] = ListBuffer[Int]()
var length: Int = 0
var hasNextGuide: Boolean = true
var useFeasibility: Boolean = true
var cutLength: Int = 0
var limitLength: Int = 10
var condition: Inequalities[K] = newInequalities(numberType)var sat: Int = 0
var solution: Expression[K] = Expression.const(num.one)var id: Int = 0
var variables: List[Symbolic[K]] = List[
Symbolic[K]]()
override def toString(): String = {var str = ""for (i <- 0 until guide.size)
str += guide(guide.size - i - 1) + ","str

A. 6 線形不等式系クラス
package es
import com.microsoft.z3._/*** This class is part of Es[Scala]* Copyright (c) 2016 Satoshi Hattori*/class Inequalities[K] (val numberType: Int) (implicit num: Numeric[K]) {var solution = Expression.const(num.one)
val context = new Context()
val solver = context.mkSolver()var variables = List[ArithExpr]()}override def toString(): String = {def nextGuide() = {solver.toString()
var next = false
var first = true
if (guide.size > limitLength)
for (i <- 0 until guide.size - limitLength)}
def makeInequality(u: Expression[K], w:
Expression[K], c: Int) = {val t = u - w
if (numberType == 0) {val t0 = t.coefs(0).asInstanceOf[Long]var zt: ArithExpr = context.mkInt(t0)for (i <- variables.size until t.coefs.
size - 1)
variables :+= context.mkIntConst(i.
toString())
for (i <- 1 until t.coefs.size) {val ti = t.coefs(i).asInstanceOf[Long]
zt = context.mkAdd(zt, context.mkMul(
context.mkInt(ti), variables(i - 1)))}
c match {case 0 => solver.add(context.mkEq(zt,context.mkInt(0)))
case 1 => solver.add(context.mkGe(zt,context.mkInt(0)))
case 2 => solver.add(context.mkLe(zt,context.mkInt(0)))
case 3 => solver.add(context.mkGt(zt,context.mkInt(0)))
case 4 => solver.add(context.mkLt(zt,context.mkInt(0)))
case 5 => solver.add(context.mkOr(
context.mkGt(zt, context.mkInt(0)),
context.mkLt(zt, context.mkInt(0))))}} else {val t0 = t.coefs(0).asInstanceOf[Double]
var zt: ArithExpr = context.mkReal(t0.
toString())
for (i <- variables.size until t.coefs.
size - 1)
variables :+= context.mkRealConst(i.
toString())
for (i <- 1 until t.coefs.size) {val ti = t.coefs(i).asInstanceOf[Double]
zt = context.mkAdd(zt, context.mkMul(
context.mkReal(ti.toString()),
variables(i - 1)))}c match {case 0 => solver.add(context.mkEq(zt,context.mkReal(0)))

case 1 => solver.add(context.mkGe(zt,context.mkReal(0)))
case 2 => solver.add(context.mkLe(zt,context.mkReal(0)))
case 3 => solver.add(context.mkGt(zt,context.mkReal(0)))
case 4 => solver.add(context.mkLt(zt,context.mkReal(0)))
case 5 => solver.add(context.mkOr(
context.mkGt(zt, context.mkReal(0)),
context.mkLt(zt, context.mkReal(0))))}}}
def solve(): Int = {var list = List[K](num.one)
val sat = solver.check()if (sat == Status.SATISFIABLE) {val model = solver.getModel()for (i <- 0 until variables.size) {// val str = model.getConstInterp(m.
getConstDecls()(i)).toStringval str = model.evaluate(variables(i),false).toString
if (numberType == 0) {list :+= str.toLong.asInstanceOf[K]} else {val numden = str.split("/")
var value = numden(0).toDouble
if (numden.size > 1)
value = value / numden(1).toDouble
list:+= value.asInstanceOf[K]}}solution = new Expression(list)
1} else {solution = new Expression(list)
0}}}