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

信学技報
TECHNICAL REPORT OF IEICE.

JML を用いた在庫管理プログラムの設計と ESC/Java2 を用いた検証
尾鷲 方志†

岡野浩三†

真二†

楠本

† 大阪大学大学院情報科学研究科 〒 560–8531 豊中市待兼山 1–3
あらまし近年，契約に基づく設計による開発手法が脚光を浴びている．これを実現する言語の一つとして JML が挙げられる．本研究では、プログラム設計の共通問題である酒屋の在庫管理問題に対して JML を用いて仕様作成を行いプログラムを記述し，ESC/Java2 を用いて実際に検証を行った．本報告では, この過程で得られた知見 (作業量,現バージョンの ESC/Java2 の記法の問題点, 解決法など) について報告する．また，ソフトウェア開発に JML を用いる上での課題について考察する.
キーワード

ESC/Java2，JML，在庫管理問題，設計検証，契約による設計A Case study — Design of Warehouse Management Program in JML
and Veriﬁcation with ESC/Java2 —Masayuki OWASHI† , Kozo OKANO† , and Shinji KUSUMOTO†† Graduate School of Information Science and Technology, Osaka University
Matikaneyama 1–3, Toyonaka-shi, 560–8531 Japan
Abstract In the software development, the notion “Design by Contract(DbC)” has been recently obtained a lotof attentions. In the DbC, contracts are represented as assertions. JML(Java Modeling Language) is one of thelanguages able to represent such assertions. In this research, we designed and programmed the Warehouse management program in Java and JML as a case study. This design is veriﬁed with “ESC/Java2”. The paper reports theknowledge about what we learned in this process. Discussion about the issue on using JML in software development
is also presented.
Key words ESC/Java2, JML, Warehouse Manaagement, Design and veriﬁcation, Design by Contract

1. ま え が きの低い段階での設計，実装に役立つ．
本事例研究では，プログラム設計の共通問題である在庫管ソフトウェアの開発手法において，従来から用いられている理問題 [10] [11] [12] についてモデル化し，JML を用いて仕様手法として V 字型モデルによる設計法 [8] がある．V 字型モデを記述した．また，実際に Java を用いてプログラムを記述しルによる設計法とは，開発における各フェーズを「設計プロセた後，ESC/Java2 を用いて検証を行い，設計と実装がともにス」と「検証プロセス」に分割し，それぞれを検証内容によっESC/Java2 において妥当であるということを示すことができて対応させたものである．

た．さらに，例外処理に関する仕様，実装の正当性に関しても

V 字型モデルによる設計法において，近年，Design by Contract(契約に基づく設計，以下 DbC とする) [1] による考え方が十分な記述をし，ESC/Java2 において妥当であるとの出力を得ることができた．

脚光を浴びている．DbC に基づいた開発では，アサーション最後に，今回の事例研究を通じて得られた知見に基づいて，により契約を示すことで，詳述段階におけるデバッグを効率化

今後の研究として他の抽象レベルの高い設計検証法などを組みされ，品質が向上する．この考え方は V 字型モデルによる設計合わせた応用例などについても述べる．

法に対して非常に有用である．

DbC を実現するための言語として JML [2] が挙げられる．
Java プログラムに対し，JML は，Java コード実体と結びつい2. 在庫管理プログラムの仕様
2. 1 概要た契約を記述することができ，ESC/Java(2) [4] [5] を用いて，酒屋の在庫管理問題に対するクラス図を図 1 に表す．受付業

コードが契約を侵す恐れがないかテストができるため，抽象度務と倉庫業務を中心とした 6 のクラスで表される．それぞれの—1—

図 1 在庫管理プログラムのクラス構成

仕様について以下にまとめる．

でなく，その中身をまとめた全品目の集合を要素として倉庫係a) 受 付 係に保持させた [11]．全品目の集合とコンテナの集合中の内蔵品

ReceiptionDesk クラスで表され，外部からの要求を受け取の合計は互いに矛盾しない．

り，倉庫に対して在庫が要求を満たすか確認させ，可能ならばその要求に含まれる商品の出庫を倉庫係に依頼し，不可能であ3. JML 記述れば未処理要求リストとして保存する．同様に，外部からコン

3. 1 JMLテナを受け付け，受け付けたコンテナを倉庫係に搬入させる．

JML とは，“Java Modeling Language” の略で，仕様を記

このとき，未処理の要求があればその要求の処理をする．外部述するための言語である [2]．JML は Java プログラムの特殊から渡されたデータを直接処理できるのは受付係のみである．

なコメント中に注釈 (アノテーション) として，Java とよく似b) 倉 庫 係

た文法で記述することができる．記述言語は基本的に Java でStorage クラスで表され，搬入したコンテナのリストをもっあり，いくつかの拡張がなされている．拡張としては、 \old,ている．受付から送られてきた要求に対し，在庫が要求を満た\result, \forall, \exists などがあり，それぞれメソッド実行前しているかどうかをかえす．また，出庫指示に対して，どのコのフィールドの値，そのメソッドの戻り値，ある条件を満たすンテナからどれだけ出庫したかを示す出庫指示書を受付に返す．

任意のフィールドの値，ある条件を満たすフィールドの値の存

全品目の集合の各要素は一意であり，また，コンテナの集合に在を意味する．

対し，各コンテナのコンテナ番号は一意である．品物の搬入はコンテナ単位で行われ，品目単位での出庫が行われる．

c) 注

文

Request クラスで表され，要素として，要求品名と要求数量，また，JML は，DbC に基づき，事前条件，事後条件などの契約により仕様を記述する [9]．JML による DbC の実現は主に以下の節を用いて実現される．

invariant クラス不変式を記述する．このクラスのオブジェク

要求者 (顧客)，さらに要求が不足している，発送済みである等トが生存中に各インスタンス変数が満たすべき契約を表す．の状態を示す値を持つ．また，一度の要求に対して要求できる

requires メソッドの事前条件を記述する．これが記述された品目は一種類のみである．

メソッドが実行されるまでに満たしているべき契約を表す．

d) 顧

客

Customer クラスで表され，顧客の住所，氏名などの個人情ソッドが実行された後に満たしているべき契約を表す．

JML は他にも，例外が起こる条件を示す “signals” 節や，無限報を持つ．

e) 品

ensures メソッドの事後条件を記述する．これが記述されたメ目

ループが起こる条件を示す “diverges” などがある．

Item クラスで表され，要素として，品名，数量の情報を持つ．

リファレンスは [3] にて公開されている．

f) コ ン テ ナ

3. 2 記 述 概 要ContainerItem クラスで表され，内蔵品の集合を持つ．各内各クラスに対して invariant 節を用いた不変条件，また，各蔵品は品目として表され，内蔵品の集合内の品目は一意である．

メソッドに対し requires 節，ensures 節を用いた事前，事後条

また，倉庫からの出庫指示に対し，内蔵品の集合の中の品目を件および，signals 節を用いて例外が起こる条件，また確実に例指定量取り出し，発送する．

外が起こり得ないことを明示した．各クラスに対しての詳細な2. 2 実装上の工夫

記述は，文献 [14] を参照のこと．記述と検証作業にかかった日

倉庫に対しての商品の搬入はコンテナ単位で行われるが，顧数は 2ヶ月ほどで，この記述を得るのに全部で 6 回のバージョ

客からの注文は品目単位で行われるため，コンテナの集合だけン変更を行っている．

—2—/∗@ public behavior/∗@ also

requires c != null;public normal behavior

assignable storage;.

ensures (\exists ContainerItem ci;.

storage.getContainerItemList().contains(ci);also

ci.getContainerID()==c.getContainerID());

public exceptional behavior

signals (Exception) false;

requires o == null;signals only java.lang.NullPointerException;@∗/
public void receiptNewContainerItem(ContainerItem c){alsopublic exceptional behavior

10storage.registContainerItem(c);requires !(o instanceof Request);deliveringOrder ();// 未発送リクエストの発送チェック

signals only java.lang.ClassCastException,}10

java.lang.NullPointerException;
signals (java.lang.ClassCastException);

図 2 例外処理を含まないメソッドの仕様記述例@∗/public /∗@ pure @∗/ int compareTo(Object o)private /∗ spec public non null ∗/ Date carryingDate;

図 4 例外処理を含むメソッドの仕様記述例

private int containerID;
private /∗ spec public non null ∗/ LinkedList itemlist;/∗ public invariant containerID >= 0;
public invariant \typeof (itemlist) == \type(Item);
public invariant (\forall Item i,j ;itemlist.contains(i) && itemlist.contains(j )&& i != j ;i.getName() !=j.getName());∗/

3. 4 例外処理記述例
図 4 に例外処理を含むメソッドの仕様記述例を示す．このメソッドは，酒屋の在庫管理問題をモデル化するにあたり定義した Request クラスのメソッドである．インターフェース

Compareble のメソッド compareTo をオーバーライドしたものであるから，also 以下に仕様記述を始める．例外の振る舞い
図 3 コンテナの不変条件

は，exceptional behavior 以下に記述する．
まず，引数が null であった場合の例外としては NullPoint-

また，これらの JML 記述が，どのような規模の Java プログ

erException を 発 生 さ せ る の で ，こ の 場 合 の 事 前 条 件 は ，ラムに対しどれだけの記述がなされたかについては表 1 にまとo == null となる．また，このときは例外が NullPointerEx-めた．

ception 以外が発生しないため，signals only 節に NullPoint-

3. 3 記 述 例

erException のみを記述した．

図 2 に例外処理を含まないメソッドの仕様記述例を示す．こまた，引数が Request 以外の型のものである場合もキャストのメソッドは，酒屋の在庫管理問題をモデル化するにあたり定処理が定義されていないので例外として扱う必要があるから，義した ReceiptionDesk クラスのメソッドで，新規コンテナの事前条件に， !(o instanceof Request) と記述し，この場合は受付処理をするメソッドである．

ClassCastException と NullPointerException が発生する可能このメソッドが呼び出し側に要求する事前の条件として，引性があるため signals only 節にそのように記述した．

数 c に有効な値が含まれていることを要求する．今回定義した

3. 5 記述の上で遭遇した問題点

クラスについて，null でなければ適当な値が入っている，もしJML 記述において，メソッド呼び出しを用いることによりくはそのオブジェクトが満たすべき本質的な性質が満たされて効率的に仕様を記述することができる．しかし，pure であるメいることが保証されている．例えば図 3 で示した今回引数とソッドしか用いることができない．pure であるメソッドとは，されるコンテナクラスの不変条件は，クラス内の各フィールド

メソッド実行の前後でオブジェクトの内部状態を変化させないが null でなく，品名は一意であり，内蔵品リストの中身は品目メソッドのことである．メソッドの事後条件を記述する場合にである Item クラスであるということが保証されている．した

おいて，あるメソッドの戻り値を用いたい場合，そのメソッドがって，ここで記述すべき事前条件は c に有効な値が入っていが pure でなければ仕様記述に使うことができない．本研究でることであるから，c! = null とだけ記述する．

は，受付の出庫処理の仕様記述において，この問題に直面した．

受け付けたコンテナは Storage.registContainerItem メソッ

これを解決する方法として考えられる方法は以下の二つが考えドにより倉庫に格納されるので，倉庫の中に存在するはずであられる．

るから，\exists を用いて storage 中の containerlist に引数で•期待した戻り値を出力する pure なメソッドを別に作る渡された c と同じ ci が存在するはずであるということを事後条•ghost ﬁeld の利用件として保証した．
また，このメソッドにより例外は起こらないので，そのように明示した．

前者の方法を用いた場合，新たなメソッドを定義することにより問題なく仕様記述を行うことができるが，実プログラム中で利用しないメソッドを仕様記述のためだけに実プログラムを用—3—

表 1 JML 設計の規模 (仮)/∗@ public ghost List tmplist;

LOC JML の LOC@∗//∗@ public behavior
assignable RequestList,storage;
ensures (\forall Request r ; RequestList.contains(r )&& (\sum ContainerItem ci;tmplist.contains(ci)&& ((Item)ci.getContainedItem().get(0)).getName().equals(r.getName());((Item)ci.getContainedItem().get(0)).getAmount())==r.getAmount();

14155

Storage242

97

ContainerItem

171

69

Request

185

87

Item

78

37

Customer

122

55

総計

939

380

10

r.getRequestState() == StockState.DELIVERED);

表 2 仕様記述に対する検証時間..

Class Name with Exception(s) without Exception(s)signals (Exception) false;@∗/
public List deliveringOrder (){..

ReceiptionDesk

7.265

7.172

Storage

9.094

9.328

ContainerItem

18.07918.125

Request4.797

4.297

Item

9.328

9.328

Customer

6.375

Total

54.938

while(i.hasNext()){..
deliveredlist.add(ReceiptionDesk

20

storage.deliveringOrder (request));54.575//@ set tmplist = deliveredlist;

ESC/Java2 は，定理証明器として一階述語論理の証明器であ
図 5 ghost ﬁeld 使用例

る “Simplify” [7] を用いている．前身のプロジェクトである

ESC/Java では不十分であった，仕様記述におけるメソッド呼いて定義するのは多くの状況において良い解決法とはならないことが多い．
ここでは ghost ﬁeld を用いた．ghost ﬁeld とは，JML 記述中のみで扱われる特殊な変数で，任意の式の値を代入しておき，仕様記述に用いることができる．図 5 に使用例を示した．ここでは，

び出しの利用の実装等が強化された．

ESC/Java2 の検証は完全でも健全でもないが [6]，比較的簡単なロジックや，型検査，例外の検査などが得意であり，デバッガとしては優秀であるとの評価がある．

4. 2 検 証 結 果

pure ではないメソッド “Storage.deliveringOrder(request r)”

文献 [14] の JML 記述に対し，ESC/Java2 を用いて一部警告の戻り値を用いたい場合に，ghost として JML 記述中に宣言さはあるものの，ほぼ全てのクラスのメソッドに対し Valid であれた tmplist に上記の戻り値を含んだ変数を，図 5 の最後のコメるとの結果を得ることができた．各クラスの検証にかかった時ント文のように set を用いて保持している．このことにより，事間は表 2 のようになった．

後条件の記述にメソッド中で “Storage.deliveringOrder(requestr)” の戻り値を保持した tmplist を用いることができるため，pure でないメソッドの戻り値を事後条件の評価に利用することができた．

5. 考

察

上記の検証結果より，例外を明示することにより検証時間が目立って増加しているわけではないことがわかる．一部のクラ一方 ghost ﬁeld を用いる場合の欠点は，メソッドをそのままスの検証に関して言うならば，検証時間が短くなっているもの用いる場合に比べ，一見した場合に意味がわかりづらいことでも見られる．このことから，[6] において言われていた，例外がある．どのメソッドからどういう値を期待しているのかという起こらない場合についてもそのことを明示すべきだ，という主ことを即座に理解するためにはできるだけメソッド呼び出しを張が数値的にも妥当である例を確認することができ，実際に明用いたほうがよいと思われる．

示することによるデメリットはないと言うことができるだろう．

また，ghost ﬁeld のように，JML 記述中のみで有効な特殊

また，仕様記述において，なメソッドを定義することもできるが，事前, 事後条件のみの\forall Object o; List.contains(i);...

定義で期待する値を表現することができない場合もあるので，のような形で各オブジェクトを参照するよりも，ここでは除外した．

4. ESC/Java2 による検証\forall int i; 0 <= i && i < List.size();List.get(i)...のように，配列を扱うようにオブジェクトを参照した方がESC/Java2 を通した検証にかかる時間が少なかった．実際に
4. 1 ESC/Java2

ContainerItem クラスの不変条件において適用した結果を表 3

ESC/Java2 における ESC は “Extended Static Checker” のに示す．他のクラスについて同様の傾向があった．

略であり，ESC/Java2 とは，JML つきの Java プログラムのSimplify の入力となる論理式では，オブジェクトのフィールサブクラスを論理式に変換し，記述されたプログラムが注釈ドを配列として表現するため [6]，配列形式を直接扱った方が定付けられた仕様に対し妥当であるかを検証するツールである．

理証明にかかる時間が少なくすむと考えられる．一方，仕様記—4—

表 3 配列形式の仕様記述にした場合の検証時間比較

ContainerItem 18.125
ContainerItem(Array) 16.891

述の観点からは前者の記述方のほうが好ましいと考えられる．

6. 今後の展望
JML が，Java のコードに結びついて，かなり詳細な設計を記述するための言語であることから，実際のプログラムコードの階層的設計法と在庫管理プログラムの開発例, 電子情報通信学会論文誌, Vol.J76-DI, No.7, pp.354-363, 1993.
[12] 二村良彦, 雨宮真人, 山崎利治, 淵一博, 新しいプログラミング・パラダイムによる共通問題の設計, 情報処理学会会誌 情報処理,
Vol.25, No.5, 1985.
[13] Daniel Jackson, Alloy: A Lightweight Object Modelling
Notation, ACM Transactions on Software Engineering andMethodology, Vol.11, Issue 2, pp.256-290, April, 2002.
[14] 尾鷲方志, 岡野浩三, 楠本真二, JML を用いた在庫管理プログラムの設計と ESC/Java2 を用いた検証の詳細例,
http://www-tani.ist.osaka-u.ac.jp/
m-owasi/esc warehouse full.pdfに縛られない，より抽象的な設計を記述できる言語を用いた付仕様記述を JML に変換する方針で研究を進めていきたいと考録えている．抽象的な設計を記述できる言語の例として Alloy や

1. 主要なクラスの JML 記述

VDM，Z 等が挙げられる．特に，Alloy は AlloyAnalyzer と

1. 1 ReceiptionDesk.javaセットになっていて，記述した仕様，またその仕様の反例を図示できるようになっていて，自動検証に強い [13]．このようなツールを用いて抽象段階での仕様の安全性が保証された設計から JML を自動生成できるようになると，手動で設計を記述する場合に比べ人為的なミスが減り，仕様，設計の信頼性の向上

package WarehouseManagement;
import java.util.∗;public class ReceiptionDesk {private /∗@ spec public non null @∗/List RequestList;に繋がる．

private /∗@ spec public non null @∗/7. ま と め

Storage storage;

本研究において，酒屋の在庫管理問題についてモデル化し，/∗@ public invariant \typeof (RequestList)

10== \type(Request);

JML を用いて仕様を記述することができた．また，実際に Javapublic ghost List tmplist;を用いてプログラムを記述し，ESC/Java2 を用いて検証を行@∗/い，設計と実装，例外処理がともに ESC/Java2 において妥当/∗@ public behaviorであるということができた．

requires r != null;

今後は 6 で述べた内容について取り組みたい．
文

requires \typeof (storage.allitemlist)

献== \type(Item);requires \typeof (storage.containerlist)[1] Bertrand Meyer, Object-Oriented Software Construction,
Second Edition, Prentice Hall, 2000.
[2] The Java Modeling Language,
http://www.cs.iastate.edu/ leavens/JML/[3] JML Reference Manual,
http://www.cs.iastate.edu/ leavens/JML/jmlrefman/jmlrefman.html[4] Extended Static Checking for Java (from Internet archive),
http://web.archive.org/
http://research.compaq.com/SRC/esc/[5] Kind Software, ESC/Java2,
http://secure.ucd.ie/products/opensource/ESCJava2/[6] David R. Cok, Reasoning with speciﬁcations containing
method calls in JML and ﬁrstorder provers, ECOOP Workshop FTfJP’2004 Formal Techniques for Java-like Programs, Oslo, Norway, June 15, 2004. ICIS report NIIIR0426, pp 41-48, 2004
[7] David Detlefs, Greg Nelson, James B. Saxe, Simplify: atheorem prover for program checking, Journal of the ACM,Vol. 52 , Issue 3, pp. 365 - 473, 2005.
[8] 開発プロセスの基本を学ぶ，
http://itpro.nikkeibp.co.jp/article/lecture/20061130/255501/?ST=develop[9] Gary T.Leavens, Yoonsik Cheon Design by Contract withJML, September 28, 2006.
[10] 大木優, 竹内彰一, 宮崎敏彦, 古川康一, 二村良彦, Concurrent
Prolog によるオンライン在庫管理システムの記述, TM0082,1984.
[11] 岡野浩三, 北道淳司, 東野輝夫, 谷口健一, 順序機械型プログラム== \type(ContainerItem);20

assignable storage, RequestList;
ensures \result== storage.checkStockSatisﬁed(r );signals (Exception) false;@∗/
public boolean receiptRequest(Request r ){if (storage.checkStockSatisﬁed(r )){storage.deliveringOrder (r );return true;}30

if (RequestList.add(r )){int tmpsize = RequestList.size();
Request tmplist[ ] = new Request[tmpsize];
Iterator i = RequestList.iterator ();for(int j =0;i.hasNext();j ++){
tmplist[j ] = (Request)i.next();}
Arrays.sort(tmplist);
RequestList.clear ();for(int j =0;j <tmpsize;j ++){

40

RequestList.add(tmplist[j ]);}return false;}
else return false;}—5—return RequestList;

110}/∗@ public behavior
assignable RequestList,storage;/∗@ public behavior

ensures (\forall Request r ;RequestList.contains(r ) 50

ensures \result == storage;&& (\sum ContainerItem ci;

assignable \nothing;tmplist.contains(ci) && ((Item)ci

signals (Exception) false;.getContainedItem().get(0))@∗/.getName().equals(r.getName());((Item)ci.getContainedItem().get(0))

public /∗@ pure @∗/ Storage getStorage().getAmount())==r.getAmount();{return storage;r.getRequestState()120}== StockState.DELIVERED);
ensures (\forall Request r ;RequestList.contains(r )/∗@ public behavior

60&& r.getRequestState()requires \typeof (storage.allitemlist) == \type(Item);== StockState.SHORTAGE ;assignable \nothing;\old(storage).checkStockSatisﬁed(r )ensures \result == storage.getItemList();signals (Exception) false;== false);
ensures (\forall Request r ;RequestList.contains(r )@∗/public /∗@ pure @∗/ List getItemList()&& r.getRequestState(){== StockState.DELIVERED130&& \old(r.getRequestState())

return storage.getItemList();}== StockState.SHORTAGE ;\result.contains(\old(storage)70/∗@ public behavior.deliveringOrder (r )));

requires \typeof (storage.containerlist)

signals (Exception) false;== \type(ContainerItem);@∗/public List deliveringOrder ()assignable \nothing;{ensures \result
Iterator i = RequestList.iterator ();== storage.getContainerItemList();

List deliveredlist = new LinkedList();signals (Exception) false;

while(i.hasNext()){

140@∗/

Request request = (Request)i.next();
if (request.getRequestState()public /∗@ pure @∗/ List getContainerItemList(){

80!= StockState.DELIVERED){

return storage.getContainerItemList();}if (storage.checkStockSatisﬁed(request)){deliveredlist.add(/∗@ public behavior

storagerequires c != null;.deliveringOrder (request));assignable storage;//@ set tmplist

ensures (\exists ContainerItem ci;= deliveredlist;
request.registAlreadyDelivered();150

storage.getContainerItemList().contains(ci);ci.getContainerID()==c.getContainerID());
signals (Exception) false;

90} else {@∗/requestpublic void receiptNewContainerItem(ContainerItem c).registShortageStock ();{requeststorage.registContainerItem(c);deliveringOrder ();// 未発送リクエストの発送チェック.getCustomer ()}.informShortageStock (request);}

160}/∗@ public behavior}
return deliveredlist;

assignable RequestList, storage;
signals (Exception) false;

100}

@∗/
public ReceiptionDesk (){/∗@ public behavior
assignable \nothing;

RequestList = new LinkedList();ensures \typeof (\result) == \type(Request);storage = new Storage();}signals (Exception) false;
@∗/}

170

public /∗@ pure @∗/ List getRequestList(){—6—