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

篩型による JML の拡張
鈴木 智大

西崎 真也

JML は Java の振舞いインタフェース仕様言語で，Java で書かれたプログラムの検証に使用される．JML はホーアが提唱した論文に基づく事前条件と事後条件による契約を記述することができる．しかし，JML はプログラムの仕様を豊富な表現で記述することができる反面，検証を行う際に必要な JML 仕様の量が多いことや，メソッドの内部での不具合の発生箇所の特定に労力が必要な場合があることなどに関して難点がある．
これらの難点を改善するために，本研究では，JML を篩型によって拡張を行う．
篩型は型に含まれる値に制約を課す述語を持つような型で，篩型を持つ変数が篩型の述語を満たすような値を常に持っていることを検証することができる．
篩型で JML を拡張する際，篩型を持つ変数のみが篩型の述語によって制約を課されることを保証するため，配列やメソッド，final で修飾されていない変数は述語に記述できないと規定する．また，JML の規則に則り，述語の中に記述される変数に対して可視性の制限を行う．
加えて，簡易的な Java 及び JML に篩型のアノテーションを加えたものである S-JML を対象として検証する
ツールの作成する．このツールは JML 仕様に対する反例の存在を SMT ソルバーを使用して検証する．また，コンストラクタでは，篩型を持つメンバー変数が篩型の述語を満たさないまま他のメソッドから使われることを防止する．
最後に，S-JML によって記述されたプログラムの例を提示し，書く必要がある JML 仕様の量の軽減と不具合の発生箇所の特定に関しての本研究に有用性があることを示す．
JML is a Java behavioral interface speciﬁcation language that is used to verify Java program codes. However, while JML can describe program speciﬁcations with rich expressions, it has some drawbacks, suchas the large amount of JML speciﬁcations required for veriﬁcation. In order to improve these diﬃculties,
we extend JML with reﬁnement types. In extending JML with reﬁnement types, we specify that arrays,
functions, and variables unqualiﬁed by the ﬁnal modiﬁer cannot be described by predicates in order toguarantee that only variables with reﬁnement types are constrained by predicates. In addition, we restrict
the visibility of variables described in predicates according to the JML rules. In addition, we develop a
veriﬁcation tool for S-JML, which is a simple version of Java and JML with reﬁnement type annotations.
This tool veriﬁes the existence of counterexamples to the JML speciﬁcation using the SMT solver. In theconstructor, it prevents member variables with reﬁnement type from being used by other functions withoutsatisfying the predicate of the reﬁnement type. Finally, we present an example of a program written in
S-JML to show the usefulness of this research in reducing the amount of JML speciﬁcations that need to be
written and in identifying where defects occur.

1 はじめに近年，Java をはじめとするオブジェクト指向のプ
ログラミング言語というのは広く使われるようになっ
JML Extension Using Reﬁnement TypeTomohiro Suzuki, 東京工業大学情報理工学院情報工学系,
Department of Computer Science, Tokyo Instituteof Technology.
Shin-ya Nishizaki, 東京工業大学学術国際情報センター,
Global Scientiﬁc and Information Computing Center, Tokyo Institute of Technology.

ている．Java は柔軟な表現ができる一方，書かれたプログラムの動作がプログラマーの想定した動作と一致しているかというのは確認するのは困難な場合が多々あり，Java で書かれたプログラムを検証するための手法というのは広く研究されている．

1. 1 仕様記述言語 JML

ソッドの終了時に不変条件//@invariant 0 < x &&Java で書かれたプログラムを検証するための手法

x < 100; と事後条件//@ensures 10 < \result &&の中の一つとして，JML(Java Modeling Language)\result < 150; を満たしていることを保証しなけれ[14] を使用して仕様を書くという手法がある．JML

ばならない．

は Java の振舞いインタフェース仕様言語で，Java のまた，メソッド method2 でメソッド method1 を呼クラスやメソッドがどのように動作するかというようび出す際には，不変条件//@invariant 0 < x && x

な仕様を明示することができる記法である．

< 100; と method1 の事前条件//@requires 10 <=最初の文字が@であるようなコメントの中に記述さarg && arg <= 50; が満たされていることを保証れることで JML 仕様であると解釈され，クラスの不しなければならないが，method1 の終了時に不変

変条件，メソッドの事前条件や事後条件などを記述す

条件//@invariant 0 < x && x < 100; と method1

ることができる．

の事後条件//@ensures 10 < \result && \result

事前条件と事後条件によるプログラムの動作の記< 150; を満たしていることが保証される．

述は，ホーア [10] により提唱された．ホーアは事前条

また，JML は実際のプログラムではコメントとし

件 P とプログラム Q，事後条件 R の関係を P {Q}Rて扱われることから，防御的なチェックを実際の動と表記し，プログラム Q の開始前に事前条件 P が真作を遅くすることなく行うことができる．例として，

であれば，Q が終了した際に事後条件 R は真になる“Design by Contract with JML” [12] から図 2 を引とした．JML はこれを基盤として，メソッドごとに用する．バイナリサーチを行うこのメソッドは引数の事前条件と事後条件を記述する．クラスの不変条件と配列の要素がソートされていることを要求している．

して記述されたことはメソッドの開始時と終了時に真しかし，配列がソートされていることを調べるためであることを意味し，すなわち全てのメソッドの事前には配列の長さに比例した時間がかかることになり，

条件かつ事後条件を意味している．

これをプログラムとして記述した場合，メソッドのJML 仕様によって記述された動作と実際の Java の処理速度を著しく低下させることになる．一方，図 2

動作が整合性があるかを検証するツールは後述の節のように JML 仕様によって記述した場合，JML を

5. 1 で紹介するツールを始めとして広く研究されてお検証するツールによってソートされている配列のみがり，Java で書かれたプログラムを検証する手段とし引数に渡されることが保証され，JML 仕様はコメンて期待されている．

トとして扱われるため実際の処理速度が遅くなるこ

JML の記述の例として，図 1 のクラス jml example

ともない．

を考える．
メ ソッド method1 で は ，3 行 目 の//@invariant

1. 2 篩型

0 < x && x < 100; が ク ラ ス jml example の 不プログラムを検証するための手法の一つとして，

変 条 件 を ，9 行 目 の//@requires 10 <= arg &&篩型 (reﬁnement type) というものが存在する [9] [20]．

arg <= 50; が メ ソッド method1 の 事 前 条 件 を ，

篩型は型に含まれる値に制約を課す述語を持つような10 行 目 の//@ensures 10 < \result && \result型である．特に，メソッドの引数や返り値の型として< 150; がメソッド method1 の事後条件をそれぞれ記篩型が使われた際には，引数や返り値の値が篩型の述述している．また，\result はメソッドの返り値を表

語を満たすことがそれぞれ事前条件と事後条件となしている．

る．篩型を持たせることで変数が想定していないよう

このとき，メソッド method1 ではメソッドの開始時な値を持つことがないかを検証することができ，プロに不変条件//@invariant 0 < x && x < 100; と事グラムの挙動を検証する手段として期待されている．

前条件//@requires 10 <= arg && arg <= 50; が篩型の例として，図 3 のような疑似コードを考え満たされていることを前提とすることができるが，メる．篩型 Nat を型として持つ変数は，int 型の値の123class jml_example {int x ;// @invariant 0 < x && x < 100;4

jml_example (){x = 50;}

5
6
7
8// @requires 10 <= arg && arg <= 50;// @ensures 10 < \ result && \ result < 150;
int method1 ( int arg ){return arg + this . x ;
}

9
10
11
12
13
14

// @ensures 10 < \ result && \ result < 150;
int method2 ( int arg ){return method1 (30);
}

15
16
17
18
19

}

図1

1
2
3
4
5
6
7
8

JML の例/* @ requires a != null
@ && (\ forall int i ;@ 0 < i && i < a . length ;@ a [i -1] <= a [ i ]);@ */int binarySearch ( int [] a , int x ) {// ...
}

12
3
4class re fi n em en t _t y pe {type Nat = { int x | x >= 0};
type NatEven = { Nat x | x % 2 == 0};
NatEven x ;5Nat method ( NatEven arg ){x = arg + 2;
return x + 5;
}

6
7
8
9

図2

防御的なチェックの例

10}

うち 0 以上の値，すなわち自然数の値を持つような

図3

篩型の例

変数であるというような制約が課せられる．また，篩
型 NatEven を型として持つ変数には，Nat 型の値の定していない値，すなわち篩型の述語を満たしていな

うち 2 で割った余りが 0 となるような値，すなわちいような値を代入する可能性があることを検知でき

偶数の自然数の値を持つような変数であるというよ

るようになり，プログラムがどこで想定していない動うな制約が課せられる．この例では，変数 x が篩型作をしたのかを特定する手段として有用であると考NatEven を持っているため，x の値が偶数の自然数だ

えられる．

という制約が課されている．

また，一度篩型を宣言すれば何度も使いまわせるこ

メソッド method には篩型によって，返り値は自然とや，NatEven で Nat が使われているように篩型を数でなければならず，引数 arg は偶数の自然数でなけ持てる変数の型として篩型を指定することで述語のればいけないという制約が課される．また，7 行目の書く量を減らすことができるため，想定された動作を

代入では，x は篩型 NatEven を持っているので，代入簡潔に記述するという点でも篩型は優れていると言される arg + 2 も偶数の自然数でなければならない．

える．

変数に篩型を持たせることによって，その変数に想1. 3 研究の目的

す NatEven の篩型を宣言している．NatEven で Nat

変数が持つ篩型の述語を満たしていることを常にが使用されているように，篩型の記述に宣言された篩

検証することは，JML での検証における不具合の発
生箇所の特定を改善するために有用である．

型名を使用することができる．
また，篩型を持つことは，図 5 のように記述する．

加えて，篩型自体が簡潔な仕様の記述という面で優図 5 では，変数 even が図 4 で宣言された NatEven

れていることや，変数が持つ篩型の述語が常に満たさという篩型を持ち，変数 nat が 0 以上の変数である

れていることが保証されていることでループの不変ことを表す篩型を持つことを示している．このよう条件などの JML 仕様を簡潔に書くことができるように，宣言された篩型名を使うことと直接篩型の記述をになることから，記述する必要のある仕様の量を減らすることはどちらも可能になっている．

すという観点でも効果的であると言える．

篩型の宣言は付録 A の S-JML の文法におけるそこで本研究は JML を篩型によって拡張すること

statement と jml-declaration において記述することによって，検証による不具合の発生箇所の特定を容易ができる．また，篩型を持つことは type-spec にて記することと，JML の記述のためにかかるコストを減述することができる．

らすことを目的するものである．

図 5 において，変数 n が持つ篩型の述語を満たす

また，簡略化した Java 及び JML に篩型を加えたというのは，n >= 0 が満たされているということでものである S-JML を検証の対象として，SMT ソル

ある．篩型の述語に含まれる x は n であるというのバーによって静的に検証するツールの作成を行った．

は優先して解釈され，もし x という変数が存在していたとしてもこの述語は n >= 0 を表す．

論文の構成
第 2 章では，どのように JML を篩型で拡張した

2. 2 篩型の述語に出現する変数と ﬁnal 修飾かについてや，篩型の述語にどのような制限を行っ

篩型の述語の中では，その篩型を持っている変数をたかについて記述している第 3 章では，拡張された除いて，final で修飾されている変数のみ使用するこJML の記述された Java のプログラムを検証するたとができるものとしている．例えば，図 6 のようなめのツールの実装について記述している．第 4 章で篩型では，変数 y は final で修飾された変数でなけ

は，JML と篩型を使用した検証対象のプログラムのればならない．

例を提示し，JML を篩型で拡張したことが有用であJava と同じくオブジェクト指向の言語である Type-ることを示している．第 6 章では結論を，第 7 章でScript に対する篩型の導入 [19] でも，immutable なは将来的に本研究に導入したい将来の課題を記述しメンバー変数のみ篩型の述語に使用できるものとしている．

ている．ここで，immutable なメンバー変数というのは，コンストラクタ以外ではそのメンバー変数を更2 篩型による JML の拡張

新することはできず，他の参照からもそのオブジェク

2. 1 篩型の記述方法

トを変化させることができない，ということを表す．

JML 仕様は最初の文字が@のコメントの中に書か本研究では，final 修飾子によって，述語に出現するれることで解釈されるが，篩型に関する仕様は ‘@か部分に関して変数が不変であることを保証している．

ら始まるコメントの中に書かれているときに解釈さまた，TypeScript に対する篩型の導入 [19] ではローれる．このため，篩型について書かれた仕様は他のカル変数に対しては immutable かどうかの判別を行JML のツールでは通常のコメントと同様に解釈されわなかったが，本研究では final で修飾されたローるため，併用することも可能となっている．

カル変数は篩型の述語に使用できるものとしている．

篩型を宣言する方法は図 4 のようになる．図 4 でこのように制限することによって，ある変数が篩型

はそれぞれ自然数を表す Nat と，自然数の偶数を表を持つことによって他の変数が制約を受けることがな12/* ‘ @def_type Nat = { int x | x >= 0 }; *//* ‘ @def_type NatEven = { Nat x | x % 2 == 0}; */

図4

1
2

篩型の宣言

int /* ‘ @ re f ine m ent _ typ e NatEven */ even ;int /* ‘ @ re f ine m ent _ typ e { int x | x >= 0 } */ n ;図5

篩型の変数への型付け

くなり，篩型の述語が満たされていることも他の変数

飾子 private で修飾されているとき，篩型の可視性に対する代入によって変化することがなくなる．例とも private として扱う．JML の spec public を記して，図 6 のような篩型を持つ変数 x は変数 y 以上述することによって変数の可視性を JML の検証におの値である必要があるが，y が final でない場合，yいてのみ public と同様に扱うことができるが，このにより大きい値を代入してしまうことが可能となり，場合には篩型の可視性も public として扱う．

その結果述語が満たされなくなってしまうことになり得る．
メンバー変数に関しても同様に final で修飾されている必要があり，例えば，図 7 の篩型では b,x,c,d,yがすべて final で修飾されている必要がある．
同様に，他の変数への代入によって述語を満たすかが変化することを防止するため，述語の中にメソッドを記述することもできないとしている．

JML では可視性について以下のような規則が定められている [14]．

• JML 仕様より狭い可視性を持つ名前を参照する
ことができない．

• JML 仕様がより広い可視性を持つメンバー変数に制約を課すことができない．
これに則り，篩型の可視性よりも可視性の狭い変数
は述語の中に書くことができないものとする．
この規則を満たしていない例として，デフォルトの2. 3 配列

可視性の変数 invalid x の持つ篩型の中に private

節 2. 2 で記述したように述語を満たすかが他の変の可視性の変数 y が含まれていた場合である図 8 を数への代入によって変化するべきではないという理由考える．

から，配列を篩型の述語に記述する際には配列の要素

このとき，他のクラスからは invalid x を参照すが final で修飾されていることが必要となる．しかることができる．しかし invalid x の持つ篩型の述しながら，配列の要素が final であることを書くこ語を検証しようとした場合，この述語には privateとはできない．これは，配列を final で修飾しても，で修飾され，他のクラスから参照することができな

その変数に新しい配列を代入することはできないだ

い y が含まれる．このように private で修飾されたけであり，配列の要素への代入は final による修飾

変数が他のクラスの検証において必要となるのは正によって制限されないためである．

しくないものとして扱われるべきである．

そのため，本研究では配列は篩型を持つことができ

一方，篩型の可視性よりも可視性の広い変数は述ず，篩型の述語の中に配列を書くことはできないもの

語の中に書くことができる．これは，篩型の述語の中としている．

に含まれる変数は final で修飾されているため，篩
型を持つ変数を参照できないクラスから篩型の述語

2. 4 可視性についてに含まれる変数を変更され，述語を満たさなくなって

篩型の可視性は，その篩型を持つ変数と同じである

しまうということが起こらないためである．よって，ものとして扱う．例えば篩型を持つ変数がアクセス修

篩型の述語は JML 仕様がより広い可視性を持つメン

1
2
3
4

class final_example1 {int /* ‘ @r efi n eme nt _ t y p e { int x | x >= y } */ x ;final int y ;
}

図6

1
2
3
4

ﬁnal での修飾の必要性 1class final_example2 {A /* ‘ @r e fin e men t _ty p e { A a | a . b . x >= this . c . d . y } */ a ;final C c ;
}

5
6
7
8
9
10
11
12
13
14
15
16
17

class A {final}class B {final}
class C {final}class D {
final
}

B b;

int x ;D d;

int y ;

図7

1
2
3
4

ﬁnal での修飾の必要性 2class in va lid_examp le {int /* ‘ @r efi n eme nt _ t y p e { int x | x >= y } */ invalid_x ;private final int y ;}図8

間違った可視性の例

バー変数を制約してはおらず，JML の可視性に関する規則の 2 つ目には当てはまらないと言える．

図 9 の例では，引数 arg は自然数であることが事前条件となり，返り値が自然数となることが事後条件となる．また，4 行目の代入においても，篩型の述語

2. 5 メソッドの事前条件，事後条件を満たす必要がある．

メソッドの返り値や引数も篩型を持つことができる．
これらの篩型はメソッドの事前条件や事後条件を表現

2. 6 エイリアス

することができる．JML の requires や ensures でJava はオブジェクト指向の言語であるので，あるもそれぞれ事前条件と事後条件を記述することがでクラスのインスタンスが複数のクラスのメンバー変

きるが，篩型の述語として記述することで返り値や引数に代入される場合がある．この場合，インスタンス数に対する事前条件や事後条件であることが明確とに対して複数のクラスが異なる篩型を持っている場合なる．また，引数の変数に対してメソッド内で代入をがある．

行った際には引数の変数の持つ篩型を検証することができる．

この際，インスタンスのメンバー変数に対して，一部のクラスに記述された篩型の述語に反する値が代1/* ‘ @def_type Nat = { int x | x>= 0 }; */

2
3
4
5
6

int /* ‘ @ re f ine m ent _ typ e Nat */ method ( int /* ‘ @ r e f i n e m e n t _ t y p e Nat */ arg ){arg = arg + 1;
return arg * arg ;}図9篩型による事前条件，事後条件の例

入される場合があるように思える．しかし，2. 2 の規

Reference Manual [14] に書かれた文法をもとに作成

則から，篩型の述語に含まれる変数は final で修飾されたものである．

されている必要があり，すなわち，上記のような代入

また，JML 仕様を書くためのコメントの記述方法

は起こりえない．また，あるクラスにおいて別のインについても，/* */で囲むような記述に限定していて，スタンスが代入される場合も考えられるが，この代入

JML の個々の記述に関しては個々に囲むものとしては他のクラスに影響を及ぼさない．

いる．例えば，図 11 の例では，事前条件と事後条件

例えば，図 10 を考える．この例のプログラムにおいて，あるクラス A，クラス B のインスタンスのメン

を 1 つの/* */で囲むのではなく，それぞれ囲む必要がある．

バー変数 c が同じクラス C のインスタンスを参照している場合を考える．A や B は c.num に対して制約を課そうとした場合，c に篩型を持たせることになる．
このとき，クラス A からはクラス B において c が篩

3. 2 ツールの実装
本研究で作成したツールは，Java を使用して書かれた検証ツールである．

型を持っていることを知ることはできないが，節 2. 2

このツールはまず，S-JML によって記述されたプより c.num は final である必要があるので，c.num

ログラムに対して構文解析を行う．この構文解析はに 1 などのクラス A に記述されている篩型の述語はパーサーコンビネーターによって実装されていて，要満たすがクラス B に記述されている篩型の述語は満素となるパーサーはクラスとして記述されている．構たさないような値を代入することは起こりえない．ま文解析の際には，それぞれのパーサーのクラスが他のた，c 自体は final で装飾される必要はないので，クパーサーのクラスをメンバー変数として保持し，木構

ラス A または B の c にクラス C の別のインスタンス

造となることで構文解析した結果を保持する．

を代入することはできるが，その場合，もう一方のクラスの c が参照するインスタンスは変化しない．

次に，構文解析の結果から，Java のプログラムがJML の仕様に反するような動作をする可能性があるかを検証する．この検証を行う際には SMT ソルバー

3 検証ツールの実装を使用していて，それぞれのパーサーのクラスに保持

3. 1 検証対象

された構文解析の結果から生成した検証条件を SMT

本研究では簡略化した Java 及び JML に篩型を加ソルバーに与えることで検証を行う．

えたものである S-JML を検証の対象としており，そ本研究のツールの検証条件の生成は OpenJML [3]の文法は付録 A に示す．簡略化の主な内容としての生成する検証条件を参考にして設計されていて，は，継承や null は S-JML に含まれないものとていプログラムを単一代入形式に変換した [1] 検証条件をる．また，扱う型を絞り，パッケージに関しても考え

SMT ソルバーに与える．例えば図 12 では，本研究ないなどの簡略化も行った．JML に関しても事前条のツールはメソッド method を 6,7 行目のような検証件や事後条件などを検証するための最低限のものだ

条件に変換し，SMT ソルバーに与える．

けを S-JML に含めている．また，この文法は JML

また，SMT ソルバーは Z3 [6] を使用した．

1
2
3

class A {C /* ‘ @r e fin e men t _ty p e { C c | c . num > 0} */ c ;
}

4
5
6
7

class B {C /* ‘ @r e fin e men t _ty p e { C c | c . num > 5} */ c ;
}

8
9
10
11

class C {final int num ;
}

図 10

1
2

エイリアスの例/* @requires num >= 0; *//* @ensures evennum % 2 == 0; */の 2 倍の値の和であり，実際の事後条件は/*@ensures

30 <= \result && \result <= 60;*/と な る ．しか し ，method2 の 検 証 で は method1 の 実 際 の 実

図 11

記述例

装 で は な く method1 の 事 後 条 件/*@ensures 10<= \result && \result <= 150;*/か ら 検 証 を 行
1234うので，method2 の事後条件も/*@ensures 10 <=void method (){int x = 0;x = x + 9;}

\result && \result <= 150;*/となる．
method1 に 記 述 さ れ て い る/*@assignable
x;*/は，このメソッドが変数 x の値を変更する可

5
6
7(= x_temp_5_0 0)(= x_temp_5_1 (+ x_temp_5_0 9))能性があることを表す．加えて，method1 が x 以外のメンバー変数の値を変更しないことを保証する．また，

図 12

単一代入形式への変換

3. 3 メソッドごとの検証

method2 は x の値を変更する可能性がある method1 を呼び出すので，method2 にも/*@assignable x;*/が記述されている．

JML は事前条件と事後条件の契約による設計を記述するために使用することができ [13]，検証はメソッ
ドそれぞれに対して別々に行うことができる．

3. 4 検証方法
篩型の述語などの JML 仕様に記述されている通り

このとき，検証中のメソッドの中でメソッドを呼びに Java のプログラムが動作するかという検証では，出す際，ツールはそのメソッドの実際の実装を利用す

SMT ソルバーによって JML 仕様を満たさないようることはできず，JML で記述された仕様のみを利用な反例が存在するかを検証する．反例が存在する場合することができる．すなわち，メソッドの呼び出し時には，メソッドの動作は JML 仕様と整合性がないとにはメソッドの事前条件や引数の篩型の述語，クラス

してその反例を出力して，次のメソッドの検証へと移の不変条件を満たしていなければならず，メソッドは行する．

事後条件やクラスの不変条件，変更可能な変数，篩型

例 え ば ，図 14 の プ ロ グ ラ ム で は ，引 数 argの述語を満たしているような動作をすることが保証が 1 で あ る と き ，6 行 目 で は 変 数 x の 持 つされるが，呼び出したメソッドがどのように実装され篩 型 の 述 語/*‘@refinement type {int x | x >ているかは検証に一切影響を及ぼさない．

1}*/を満たさないような代入が行われることにな

例えば，図 13 では，メソッド method2 の実際の返り値は引数 arg の値とメンバー変数 x に代入された arg

る．本研究のツールは，これを反例として見つけることができる．

12
3class jml_example {int x ;/* @invariant 0 < x && x <= 100; */4

jml_example (){x = 50;}

5
6
7
8/* @requires 10 <= arg && arg <= 50; *//* @ensures 10 <= \ result && \ result <= 150; *//* @assignable x ; */int method1 ( int arg ){x = arg * 2;return arg + this . x ;
}

9
10
11
12
13
14
15
16

/* @requires 10 <= arg && arg <= 20; *//* @ensures 10 <= \ result && \ result <= 150; *//* @assignable x ; */int method2 ( int arg ){return method1 ( arg );
}

17
18
19
20
21
22
23

}

図 13

1
2

メソッドごとの検証の例

class v_example {int /* ‘ @r efi n eme nt _ t y p e { int x | x > 1} */ x ;3/* @requires arg > 0; */void set_x ( int arg ){x = arg ;
}

4
5
6
7
8

}

図 14

また，篩型の述語に final で修飾されていない変検証の例とによって変わることはない．

数が含まれるなど，Java のプログラムや JML 仕様

また，後述のコンストラクタに関する検証 (節 3. 7)が不当なものである場合には，本研究のツールは処理

では，コンストラクタ以外のメソッドからメンバー変中のメソッドは不当なものであるとしてその内容を出数の持つ篩型の述語を参照することが可能となる前

力し，次のメソッドの検証に移行する．

に，篩型の述語を満たしているかどうかの検証を行っている．そのため，メンバー変数の持つ篩型の述語は

3. 5 篩型の検証

その変数を持つインスタンスのコンストラクタ内以

本研究のツールでは，篩型の述語を満たしているか

外では常に満たしていることが保証されている．

の検証は，篩型を持つ変数に対して代入を行うときに

例えば，図 15 では 6 行目の代入において，代入後行う．篩型の述語に使用できる変数は final で修飾に変数 y が持つ篩型の述語が満たされているかの検された変数のみであるため，述語を満たしているかど証が行われるが，変数 x が常に 5 よりも大きい値でうかは篩型を持つ変数以外の変数の値が変化するこあることが篩型の述語によって保証されているため，

変数 y の持つ篩型は満たされることを検証することができる．

回でなければならない．

final で修飾された変数が持つ篩型の述語は，その変数自体も，述語に含まれる他の変数も全て final

3. 6 ループするような述語で修飾されていることになる．すなわち，値が初期化

図 16 の例を考える．クラス A の x a の持つ篩型のされた後，述語による制約を満たしているかどうかと述語にはクラス B の x b が含まれていて，この変数はいうのは変わることがないと言うことができる．

篩型を持つ．クラス B の x b の持つ篩型の述語にはク

そのため，本研究のツールでは，final で修飾されラス A の x a が含まれ，前述のとおり篩型を持ってた変数に値が代入された時点ではその変数が持つ篩

いる．そのため，篩型の検証を行おうとすると，ルー型の述語に対する検証は行わず，節 3. 7. 1 と合わせプが発生してしまい，検証が困難になってしまう．

てコンストラクタの終了時に，final で修飾されてい本研究のツールでは，篩型の検証の深度を制限する

るかに関わらず，そのクラスのメンバー変数に対してことでこの問題に対処をしている．すなわち，一定回

篩型の述語を満たしているかの検証を行っている．

数以上ループを繰り返した篩型の述語内に含まれる

このような検証方法を取ることで，図 17 のような変数は篩型を持っていたとしても篩型を持っていない

篩型の記述でも正しく動作していることを本研究のとして扱って検証を行う．また，この深度の最大値は

ツールは検証することができる．

ツールを使用するユーザーが設定できるものとして

3. 7. 3 メソッド呼び出し

いる．

コンストラクタの中でメソッドを呼び出す場合を考える．

3. 7 コンストラクタ

自身のインスタンスのメソッドを呼び出す場合，そ3. 7. 1 自動的に初期化された値のメソッドはメンバー変数全てが篩型を満たしている

Java の挙動として，コンストラクタの開始時に intという前提で動作が正しいことが検証によって保証さや boolean の変数に 0 や false が代入される．これれる．そのため，呼び出したメソッドが正しく挙動をらの値が篩型の述語を満たすことは必要ではない．

していることを保証するために，コンストラクタ内で本研究のツールでは，それらの変数に値が代入され自身のインスタンスのメソッドを呼び出す前に全てのることなく使用された場合には，0 や false が篩型

メンバー変数の持つ篩型に対して述語を満たしていの述語を満たしていないような反例が存在することるかの検証を行う．

を検知することができる．しかし，0 や false がそのこのとき，節 3. 7. 4 のような場合を除き，他のイ

変数の篩型の述語を満たしていない反例が存在する，

ンスタンスからコンストラクタのインスタンスのメ

かつ，一度も使用されずにコンストラクタが終了する

ンバー変数を参照することはできないため，他のイン場合，コンストラクタの終了時点で篩型の述語を満たスタンスのメソッドを呼び出す際にはコンストラクタ

していない変数が存在することを検知できない可能のインスタンスのメンバー変数が持つ篩型の述語を性も存在する．

満たしている必要はない．

そのため，本研究のツールではこのような可能性を

3. 7. 4 this キーワード

検知するために，コンストラクタの終了時に，そのク

コンストラクタの処理中に，this を他のインスタ

ラスの全てのメンバー変数に対して篩型の述語を満ンスが参照可能な変数に代入したり，他のインスタン

たしているかの検証を行っている．

スのメソッドの引数に this を渡したりする場合，こ3. 7. 2 ﬁnal で修飾された変数の篩型の検証の this は篩型を満たしていないメンバー変数を持つ

コンストラクタではそのクラス自身の final で修可能性があることになる．すなわち，篩型の述語を満飾されたメンバー変数に対して必ず代入をして初期

たしていない変数が存在する状態で，他のメソッドか化しなければならず，また，その代入の回数は必ず 1

ら this を参照することが可能となり，メソッドの呼12
3

class r e f i n e m e n t _ t y p e _ e x a m p l e {int /* ‘ @r efi n eme nt _ t y p e { int x | x > 5} */ x ;int /* ‘ @r efi n eme nt _ t y p e { int y | y > 3} */ y ;4void method (){y = x;
}

5
6
7
8

}

図 15

1
2
3
4
5
6
7

篩型の検証の例

class A {final int /* ‘ @re fin e m e n t _ t y p e { int x | x > b . x_b } */ x_a ;final B b ;void method (){/* @assert x_a > 1; */
}
}

8
9
10
11
12

class B {final int /* ‘ @re fin e m e n t _ t y p e { int x | a . x_a > x && x > 0} */ x_b ;final A a ;
}

図 16

1
2
3

ループするような述語の例

class final_example {final int /* ‘ @re fin e m e n t _ t y p e { int x | x > y } */ x ;final int /* ‘ @re fin e m e n t _ t y p e { int y | x > y } */ y ;4

final_example (){x = 2;
y = 1;
}

5
6
7
8
9

}

図 17

コンストラクタによる ﬁnal で修飾された変数の篩型

び出し時に全ての変数の持つ篩型の述語は満たされているという前提を保証できないことになってしまう．

行う．
ループの検証は以下のように行う．

このような状況を防止するため，コンストラクタ• for 文の初期化を行い，このときにループの継続

内で this を使用する際には，その時点で全てのメン

条件を満たしているならば，ループの不変条件を

バー変数が持つ篩型の述語を満たしていることを検満たしていないような反例が存在しないことを証している．

検証する．このとき，for 文の初期化とはローカ
ル変数の宣言であり，もしこのローカル変数が篩

3. 8 ループ型を持つ場合には，その述語が満たされているか

メソッド内で for 文が記述されている場合には，の確認を行う．

JML で記述されたループの不変条件をもとに検証を• ループの不変条件とループの継続条件が満たされていること，及び全ての変数が持つ篩型の述語を参考にして書かれていて，一部引用している．

が満たされていることを仮定して，変数の値に関Java のプログラムと JML 仕様に整合性がないな

わらず，ループの中身を処理した後にループの不らば本ツールは警告を出すことができるか

変条件を満たしていないような反例が存在する• 本研究では簡略化した Java 及び JML であるかを検証する．

S-JML を検証の対象としており，そのため，本ループ内の処理は，ループの不変条件とループの来であれば想定しない動作であるものを検知で継続条件，全ての変数が持つ篩型の述語が開始時きない場合がある．例えば，null は S-JML に含に満たしていることのみを前提とする．そのた

まれていないため，本研究のツールは null を参め，篩型を持つ変数に対して代入をする際には，照していることを検知することができない．

その前提から述語を満たさない反例が存在しな• 事前条件などの仕様が誤っていた場合，パス条

いことを検証できる必要がある．

• 反例が存在しなければループは正しく動作して件を満たさないようになり，反例を見つけることができなくなってしまう可能性がある．例えいると検証できることになる．このとき，ループ

ば，図 18 では，/*@assert x == 5;*/で反例がの終了時には，ループの継続条件が満たされてい見つかることが期待される．しかし，これを検ないことと，初期化時にループの継続条件が満た証しようとした場合，(x > 0) && (x < 0) &&されているのならばループの不変条件が満たさ￢ (x == 5) が検証されることになり，これを満れていることが分かる．

たすような x は存在しない．このため，本研究

ここで，篩型の述語はループの開始時と終了時のどちらでも満たしていることが保証されるので，篩のツールでは到達不可能になるような制約が加えられてないかの検証を行っている．

型の述語に記述されていることはループの不変条件• 本ツールは検証中のメソッド以外のメソッドにとして書く必要がなくなる．このことにより，記述す

ついて，その Java のプログラムと JML 仕様にる JML の量を減らすために篩型は非常に効果的であ

整合性があることを前提として検証を行っている．また，この記述量の減少は for 文が複数存在する

る．そのため，他のクラスの JML に誤りがあっときに特に顕著であると考えられる．

た場合，本来警告を出すべきであっても検知することができない場合がある．例えば，図 19

3. 9 健全性と完全性

では，method2 の返り値は 2 であるにも関わら本研究のツールは可能な限り健全性や完全性を持っす，JML の事後条件は返り値が 5 よりも大きて検証を行うツールになることを目標としているが，いと記述されている．このとき，method1 の実

このような検証のツールは健全性や完全性を持たせ際の返り値も 2 であるが，method1 は method2

ることは難しい．

の実際の実装を確認することなく，JML 仕様で

ここで，健全でないというのは，Java のプログラある事後条件/*@ensures \result > 7;*/のみ

ムと JML 仕様に整合性がないにも関わらず，本研究から検証を行う．そのため，method1 の事後条のツールが警告を出すことができない場合があると

件/*@ensures \result > 5;*/は満たしているいうことである．また，完全でないというのは，本研と検証される．ただし，この場合，本研究のツー

究のツールが警告を出すにも関わらず，Java のプロ

ルは method2 に対して警告を出すことができ，グラムと JML 仕様に整合性がある場合があるという

method2 の事後条件を修正すれば method1 に対ことである [15]．

して本研究のツールは警告を出すことができる

節 3. 9，節 3. 9 はそれぞれ現時点での本研究のツーようになる．

ルの現時点での健全性，完全性に関するものであり，• 本来，全てのクラスの不変条件や篩型の述語は，OpenJML [3] や ESC/Java [15] における同様の議論

メソッドの開始時に満たされているいることが必要となる．しかし，節 3. 6 で説明した場合から1わかるように，実際には全てにおいて満たされて 2いることを検証することはできず，警告を出すの 3
4に十分な制約を得ることができない場合がある．5• 本研究のツールは SMT ソルバーを使用して検 67証を行っているが， SMT ソルバーが推論で用い 8class false_path {/* @requires x > 0; */void method ( int x ){if ( x < 0){/* @assert x == 5; */}}}る SAT 問題検証器は，SAT 問題が NP 問題であることから考えても，非常に計算量が高くなるこ

図 18

パス条件が満たされないような場合ともあり，SMT ソルバーが利用可能な時間やメ
モリを使い果たしてしまう場合があるが，その場合は仕様に反例が存在するかが検証できない．

1
2• また，本研究のツールは，オーバーフローやエ34

イリアスの検証などを始めとして，将来の課題と 5class false_other {/* @ensures \ result > 5; */int method1 (){return method2 ();}してまだ実装されていない機能が存在し，そのた 6/* @ensures \ result > 7; */int method2 (){return 2;}

7

めに本来出すべき警告を出すことができない場 8
合がある．

9
10

本ツールは警告を出すならば Java のプログラムと11}JML 仕様に整合性がないか• 本研究では S-JML を検証の対象としているた

図 19

他のメソッドが間違っている場合

め，その中に含まれていない文法を含んだ検証対
象は，それが正しいものだったとしても警告を出

4 応用例してしまう．

• 無限ループを避けるなどのために本来は反例で

4. 1 篩型による不具合の発生箇所の特定の例

ないものが反例として出力される場合がある．こ本研究のツールで効果的な検証を行うことができ

れは \forall などを含んだ JML 仕様を検証する一例として，図 20 のようなプログラムを提示する．

る際などに起こりうる．現在 S-JML の文法には

この例では，事前条件/*@requires num >= 0;*/に含まれていないが，将来的に導入する際にはこのよって 0 以上であることが保証されている引数 num

不完全性が発生する可能性がある．

を取り，引数 num 以上の偶数のうち最も小さい 2 つの• 本研究のツールが生成する検証条件は，Java の偶数をクラス Even のメンバー変数 evennum に足す．

意味論を完全にモデル化することはできておらこのプログラムを書く際，，例えば 10 行目の if 文の条件をず，そのために正しく動作していても警告を出す
場合がある．

1

if ( num %2==0){• 本ツールではメソッドごとに検証を行っていて，メソッドを呼び出す際には JML 仕様のみによりと書いてしまう間違いというのは十分に考えられる検証を行っているため，仕様が不十分にしか記述ものである．しかしながら，間違えたプログラムでされていない場合には，正しく動作していたとしは evennum に 2 回奇数を足す処理を行うことになり，ても警告を出す場合がある．

事後条件では偶数になってしまうため，誤りに気付くことが難しくなってしまう．
ここで，even や evennum に偶数の自然数であるという篩型を持たせることにより，意図していない処理を行っていることを本研究のツールは検証することができる．

JML の assert はメソッドのある時点で述語を満

5 関連研究5. 1 JML

たすことを記述することができるが，この例がより

JML の設計などについては，“Preliminary Design

長く複雑なものだった場合，全ての even や evennum

of JML” [12] や “JML Reference Manual” [14] 等に書の代入に対して assert 節を書くというのは保守性やかれている．

書かなければいけない JML 仕様の量などの理由で現実的でない．

ホーアの論文 [10] を基盤とした事前条件と事後条
件の契約による設計を JML によって記述すること

この点で，篩型を使用すれば同様のことを少ないについては Leavens らの “Design by Contract withJML 仕様の量で記述することができ，非常に有用でJML” [13] に記述されており，本研究のツールはこのある．また，例えば evennum が整数の偶数である，と考え方に基づき，メソッドごとに検証を行っている．

いうような変更を行ったとしても，evennum の持つJML を使用して Java のプログラムを検証するツー

篩型を変更するだけで対応することができるので，保ルには，自動定理証明器の Simplify [7] を使用して検守性としても優れていると言える．

証を行う ESC/Java2 [4] や，SMT ソルバーを使用して検証を行う前述の OpenJML [3] などが存在する．

4. 2 篩型によりループの不変条件の記述を簡潔にしている例

また，KRAKATOA [16] は JML から WHY [8] を使用して証明支援システムの Coq [5] の証明責務を生図 21 は，返り値が 3 の倍数となるようなメソッド

成することで検証を行うツールである．Coq は SMTの例である．メソッド method1 とメソッド method2

ソルバーよりも検証できる表現が多いが，検証の自動は，JML 仕様は異なるが Java の実装部分は全く同化や JML 仕様と Java プログラムの不整合の箇所のじものである．また，事後条件/*@ensures \result

特定などが困難であるという違いがある．

% 3 == 0;*/も同じものであり，返り値が 3 の倍数であることが記述されている．

5. 2 篩型

method1 で は ，返 り 値 が 3 の 倍 数 で あ る こ

篩型が初めて導入されたのは，ML の拡張 [9] としと を 検 証 す る た め に ，そ れ ぞ れ の ル ー プ に 対てである．この研究では，型推論の決定可能性などのし て 変 数 mul of 3 が 3 の 倍 数 で あ る と い う

ML の性質を維持したまま，より多くのエラーを検出

ル ー プ の 不 変 条 件/*@maintaining mul of 3 % 3することを目的としていた．

== 0;*/を JML 仕様として記述することが必要となる．
一方，method2 では mul of 3 が 3 の倍数であることは篩型の述語として記述されている．このとき，その後，篩型は Haskell [18] 等の関数型言語に導入する研究がなされている他，近年ではオブジェクト指向言語である TypeScript [19] や，Scala [17] に導入す
る研究もなされている．

ループの処理中であっても篩型の述語は常に満たさ

本研究では篩型を静的に検査したが，動的な検査にれるので，mul of 3 が 3 の倍数であるということは利用することも研究されている．Knowles らによる

ループの不変条件として書く必要はなくなり，より簡Hybrid Type Checking [11] では，静的な検査と動的

潔かつ保守性が高いような記述ができていることがな検査を組み合わせ，より効率的な検証を実現して言える．

いる．JML は動的な検査のために使用することもで
き [2]，これらの組み合わせによってより優れた検証を行うことができる可能性は十分に考えられる．

1
2
3
4

class Even {/* ‘ @def_type Nat = { int x | x >= 0}; *//* ‘ @def_type NatEven = { Nat x | x % 2 == 0}; */int /* ‘ @r efi n eme nt _ t y p e NatEven */ evennum ;5/* @requires num >= 0; *//* @ensures evennum % 2 == 0; */int addTwoEven ( int num ){int /* ‘ @r e fi nem e n t _ t y p e NatEven */ even = 0;
if ( num %2==1){even = num + 1;
} else {even = num ;
}

6
7
8
9
10
11
12
13
14
15

this . evennum = this . evennum + even ;even = even + 2;
this . evennum = this . evennum + even ;return this . evennum ;

16
17
18
19

}

20
21

}

図 20

検証するプログラムの例 1

ムの不具合の発生箇所を発見しやすくなる例と JML

6 結論の記述量を減らすことができる例を提示し，本研究の本研究では，JML を篩型によって拡張を行った．そ

有用性を示した．

の際，篩型の述語に対しては，配列やメソッド，final
で修飾されていない変数などの記述を禁じ，篩型の述

7 今後の展望

語によって制約されるのは篩型を持つ変数のみとなる

本研究のツールで検証できるのは S-JML に関してようにしている．また，JML の可視性に関する規則

であり，検証できる対象を広げるのが今後の最も優先に基づき，篩型を持つ変数の可視性よりも狭い可視性

するべき課題となっている．

を持つ変数は記述できないとしている．

仕様記述の部分，すなわち，JML に関しては “JML

加えて，本研究では簡略化した Java 及び JML に

Reference Manual” [14] の Level 0 Features に記載さ篩型を加えたものである S-JML を静的に検証するれた特性から順に検証を可能とすることを当面の目

ツールの実装を行った．主な簡略化としては，継承標とする．

や null は S-JML に含まれないものとした．また，扱う型を絞り，パッケージに関しても考えないなどの簡略化も行った．このツールは SMT ソルバーを使用

また，プログラム記述部分，すなわち，Java に関しては，• null リテラルの導入

し，JML 仕様に対する反例が存在しないかどうかを– null を導入して，NullPointerException がメソッドごとに検証を行う．検証時には常に篩型の述発生の有無を検証する手法を研究する．

語を満たしていることを仮定していて，コンストラク• 継承の導入

タではメンバー変数が篩型の述語を満たさないまま– 継承は，オブジェクト指向プログラミング

他のメソッドから使われることを防止するような処理

言語パラダイムにおける中心的な概念であを行った．

る．継承を導入したもとで検証が可能である

最後に，本研究のツールを使用することでプログラ

どうかを研究することが重要である．

1class example_loop {2/* @ensures \ result % 3 == 0; */int method1 (){int mul_of_3 = 0;/* @maintaining mul_of_3 % 3 == 0; */for ( int i = 0; i < 10; i = i + 1){
mul_of_3 = mul_of_3 + 3;}/* @maintaining mul_of_3 % 3 == 0; */for ( int i = 0; i < 10; i = i + 1){
mul_of_3 = ( mul_of_3 - 2) * 3;}/* @maintaining mul_of_3 % 3 == 0; */for ( int i = 0; i < 10; i = i + 1){
mul_of_3 = mul_of_3 - 6;}
return mul_of_3 ;
}

3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

/* @ensures \ result % 3 == 0; */int method2 (){int /* ‘ @r e fi nem e n t _ t y p e { int x | x % 3 == 0} */ mul_of_3 = 0;
for ( int i = 0; i < 10; i = i + 1){
mul_of_3 = mul_of_3 + 3;}
for ( int i = 0; i < 10; i = i + 1){
mul_of_3 = ( mul_of_3 - 2) * 3;}for ( int i = 0; i < 10; i = i + 1){
mul_of_3 = mul_of_3 - 6;}
return mul_of_3 ;
}

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

}

図 21

検証するプログラムの例 2• エイリアスの検証– エイリアスされている可能性のある変数に対する代入は，同じ型を持つ他の変数の値も変化させる可能性がある．このことを検知できないことはツールが健全でない要素の一つとなるので，エイリアスの検証は優先的に導入することが求められる．

• オーバーフローなどの検証– オーバーフローは数値の計算において意図– static は Java では main メソッドの修飾子として必須であり，S-JML に導入する必
要がある．

• ++や単項演算子としての-など，使用できる演算子の増加– 現在 S-JML に含まれているのは最低限の演算子のみであり，より多くのプログラムを検証できるようになるために導入は必要である．

しない動作を引き起こす原因の一つであり，などに関して，特に優先的に S-JML に導入を行う必

検証する必要がある．

要があると考えている．

• static 修飾子の導入

JML 仕様を書くためのコメントの記述方法に関し

て，本研究のツールは節 3. 1 で述べたような限定的な方法でしか対応していないが，記述方法を JML と同様にすることも課題である．
配列に関しても，将来的には篩型を持つことができるようにすることを検討している．実現するための手法としては，配列の要素に再代入がされないことを記述することができるようにする，配列の全ての要素が同一の篩型を満たしていることを記述できるようにする，などの手法が考えられる．
加えて，ツールの高速化も今後の課題の 1 つである．変数の値が変化していないにも関わらず同じ変数の篩型の制約を SMT ソルバーに何度も与えてしまっているなど無駄な処理が多い．これが処理速度の低下を招いている可能性がある．重複する処理は行わな
いようにすることにより，改善を図ることが必要であろう．
謝辞
有用で素晴らしい議論をしてくださった西崎研究室の皆様のおかげです．厚く御礼申し上げます．また，論文の執筆の際に，精神的にも支えてくださった友人や家族の皆様には深く感謝いたします．

参 考 文 献[ 1 ] Barnett, M. and Leino, K. R. M.: Weakestprecondition of unstructured programs, PASTE,(2005), pp. 82–87.
[ 2 ] Cheon, Y. and Leavens, G. T.: A Runtime Assertion Checker for the Java Modeling Language(JML), SERP, CSREA Press, 2002, pp. 322–328.
[ 3 ] Cok, D. R.: OpenJML: Software veriﬁcation forJava 7 using JML, OpenJDK, and Eclipse, EPTCS
149, (2014), pp. 79–92.
[ 4 ] Cok, D. R. and Kiniry, J.: ESC/Java2: Uniting
ESC/Java and JML, CASSIS, (2004), pp. 108–128.
[ 5 ] Coq development team: The Coq proof assistantreference manual V8.13, https://coq.inria.fr/refman/,2020.
[ 6 ] de Moura, L. and Bjørner, N.: Z3: An Eﬃcient
SMT Solver, TACAS, (2008), pp. 337–340.
[ 7 ] Detlefs, D., Nelson, G., and Saxe, J. B.: Simplify: a theorem prover for program checking, Journal of the ACM, Vol. 52, No. 3(2005).
[ 8 ] Filliâtre, J.-C.: The Why certiﬁcation tool,
http://why.lri.fr/.
[ 9 ] Freeman, T. and Pfenning, F.: Reﬁnement
Types tor ML, PLDI, (1991), pp. 268–277.
[10] Hoare, C. A. R.: An axiomatic basis for computer programming, Communications of the ACM,
Vol. 12, No. 10(1969), pp. 576–583.
[11] Knowles, K. and Flanagan, C.: Hybrid Type
Checking, ACM TOPLAS, Vol. 32, No. 2(2010).
[12] Leavens, G. T., Baker, A. L., and Ruby, C.: Preliminary design of JML: a behavioral interface speciﬁcation language for java, ACM SIGSOFT Software
Engineering Notes, Vol. 31, No. 3(2006).
[13] Leavens, G. T. and Cheon, Y.: Design by Contract with JML, (2006).
[14] Leavens, G. T., Poll, E., Clifton, C., Cheon, Y.,
Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.,
Zimmerman, D. M., and Dietl, W.: JML Reference
Manual, (2013). DRAFT Revision 2344.
[15] Leino, K. R. M., Nelson, G., and Saxe, J. B.:
ESC/Java User’s Manual, Technical Note 2000-002,
Compaq SRC, (2000).
[16] Marché, C., Paulin-Mohring, C., and Urbain,
X.: The KRAKATOA tool for certiﬁcation of
JAVA/JAVACARD programs annotated in JML,
The Journal of Logic and Algebraic Programming,Vol. 58(2004), pp. 89–106.
[17] Schmid, G. S. and Kuncak, V.: SMT-Based
Checking of Predicate-Qualiﬁed Types for Scala,
SCALA, (2016), pp. 31–40.
[18] Vazou, N., Seidel, E. L., Jhala, R., Vytiniotis,
D., and Peyton-Jones, S.: Reﬁnement Types For
Haskell, ICFP, (2014), pp. 269–282.
[19] Vekris, P., Cosman, B., and Jhala, R.: Reﬁnement Types for TypeScript, PLDI, (2016), pp. 310–
325.
[20] Xi, H. and Pfenning, F.: Dependent Types inPractical Programming, POPL, (1999), pp. 214–
227.

ensures-clause | assignable-clause

A 付録: 検証対象の文法 S-JML
compilation-unit ::= [class-declaration ] . . .
class-declaration ::= class ident class-block
modiﬁers ::= [modiﬁer ] . . .
modiﬁer ::= private | ﬁnal | jml-modiﬁer

spec-header ::=requires-clause [ requires-clause ] . . .
compound-statement ::={ statement [ statement ] . . . }statement ::= compound-statement

jml-modiﬁer ::= spec public| local-declaration ;ident ::= letter [ letter-or-digit ] . . .

| expression ;letter ::= , $, a through z, or A through Z| if ( expression ) statement

digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9[ else statement ]letter-or-digit ::= letter | digit| return [ expression ] ;class-block ::= { [ ﬁeld ] . . . }| assert-statementﬁeld ::= member-decl| possibly-annotated-loop| jml-declaration
jml-declaration ::= [ private ] invariant| def type-clausemember-decl ::= method-decl| variable-deﬁnition
method-decl ::= [ generic-spec-case ]| def type-clausepossibly-annotated-loop ::=[ loop-invariant ] . . .
loop-stmt
loop-invariant ::= maintaining-keyword predicate ;maintaining-keyword ::= maintaining

modiﬁers [ type-spec ] method-head

spec-expression ::= expression

compound-statement

local-declaration ::= variable-decls

type-spec ::=type [ dims ] [ reﬁnement type-clause ][ assignment-op implies-expr ]assert-statement ::= assert predicate ;type ::= reference-type | built-in-type

expression-list ::= expression [ , expression ] . . .

reference-type ::= ident

loop-stmt ::= for ( [ local-declaration ] ;built-in-type ::= void | boolean | int[ expression ] ; [ expression-list ] ) statement

dims ::= ‘[’ ‘]’requires-clause ::= requires predicates ;method-head ::= ident formals

ensures-clause ::= ensures predicates ;formals ::= ( [ param-declaration-list ] )assignable-clause ::= assignable store-ref-list ;param-declaration-list ::=store-ref-list ::= \nothing

param-declaration [, param-declaration ] . . .
param-declaration ::= [ ﬁnal ] type-spec ident
variable-deﬁnition ::= modiﬁers variable-decls ;variable-decls ::= type-spec ident
generic-spec-case ::=spec-header [ simple-spec-body ]| simple-spec-bodysimple-spec-body ::= simple-spec-body-clause[ simple-spec-body-clause ] . . .
simple-spec-body-clause ::=| store-ref-expression [ , store-ref-expression ]. . .
store-ref-expression ::= store-ref-name[ store-ref-name-suﬃx ] . . .
store-ref-name ::= ident | thisstore-ref-name-suﬃx ::= . ident|[

spec-array-ref-expr]

spec-array-ref-expr ::= spec-expression
invariant ::= invariant predicates ;predicate ::= spec-expression

expression ::= assignment-expr
assignment-expr ::= [ postﬁx-expr assignment-op ]implies-expr
assignment-op ::= =implies-expr ::= logical-or-expr[ ==> implies-expr ]logical-or-expr ::= logical-and-expr[||

logical-and-expr ] . . .

primary-expr [ primary-suﬃx ] . . .
primary-suﬃx ::= .ident| ( [ expression-list ] )|[expression]

primary-expr ::= ident | new-expr| java-literal | this| ( expression )| jml-primary

logical-and-expr ::= equality-expr

new-expr ::= new type new-suﬃx[ && equality-expr ] . . .

new-suﬃx ::= ( [ expression-list ] )equality-expr ::= relational-expr[ == relational-expr ]| relational-expr [ != relational-expr ]relational-expr ::= additive-expr < additive-expr|[

expression]

java-literal ::= integer-literal| boolean-literal
integer-literal ::= 0 | non-zero-digit [ digit ] . . .

| additive-expr > additive-expr

non-zero-digit ::= 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9| additive-expr <= additive-expr

boolean-literal ::= true | false| additive-expr >= additive-expr

jml-primary ::= result-expression| additive-expr
additive-expr ::= mult-expr[ additive-op mult-expr ] . . .
additive-op ::= + | mult-expr ::= postﬁx-expr[ mult-op postﬁx-expr ] . . .
mult-op ::= * | / | %postﬁx-expr ::=| old-expression
result-expression ::= \result
old-expression ::= \old ( spec-expression )def type-clause ::=def type ident = reﬁnement type ;reﬁnement type ::= { type ident ‘|’ predicates }reﬁnement type-clause ::= reﬁnement type ident| reﬁnement type reﬁnment type