研究速報
在庫管理プログラムの設計に対する JML 記述とESC/Java2 を用いた検証の事例報告
尾鷲 方志†楠本岡野 浩三†（正員）

真二†（正員）Design of Warehouse Management Program in JML and its Veriﬁcation with ESC/Java2Masayuki OWASHI† , Nonmember, Kozo OKANO† , andShinji KUSUMOTO† , Members†

大阪大学大学院情報科学研究科〒 560–8531 大阪府豊中市待兼山

Graduate School of Information Science and Technology, Osaka University, Toyonaka-shi, 560–8531 Japan

Fig. 1図 1 在庫管理プログラムのクラス構成
Class diagram of warehouse management program

あらまし
本稿では，契約に基づく設計が行える JML を用いて確認させ，可能ならその要求された商品の出庫を倉庫在庫管理問題の仕様作成を行い，ESC/Java2 を用い係に依頼し，不可能ならば未処理要求リストとして保て検証した．この結果や考察について述べる．

存する．同様に，外部からコンテナを受け付け，倉庫キーワード ESC/Java2，JML，在庫管理問題，設計検証，契約による設計

1. ま え が き係に搬入させる．このとき，未処理の要求があればその要求の処理をする．外部から渡されたデータを直接処理できるのは受付係のみである．

Design by Contract(契約に基づく設計，以下 DbC

倉庫係は Storage クラスで表され，搬入したコンテとする) [1] に基づいた開発では，表明により契約をナのリストを持つ．受付から送られてきた要求に対し，示すことで詳述段階におけるデバッグが効率化され，在庫が要求を満たしているかどうかを返す．また，出品質が向上する．DbC を実現するための言語である

庫指示に対して，どのコンテナからどれだけ出庫した

JML は，Java プログラムに対しコード実体と結びつかを示す出庫指示書を受付に返す．全品目の集合の各いた契約を記述することができ，ESC/Java または要素は一意であり，また，コンテナの集合に対し，各ESC/Java2 を用いてコードが契約を侵す恐れがないコンテナのコンテナ番号は一意である．品物の搬入はかを検証することができる．

コンテナ単位で行われ，品目単位での出庫が行われる．

本稿では，プログラム設計の共通問題である在庫管注文は Request クラスで表され，要素として品名と理問題 [3] について，JML を用いて仕様を記述した．

数量，要求者 (顧客)，さらに要求が不足している等の

また，実際に Java を用いてプログラムを記述した後，状態を示す値を持つ．一度に要求できる品目は一種類

ESC/Java2 を用いて検証を行い，設計と実装がとものみである．に ESC/Java2 において妥当であることを一分程度で2. 2 実装上の工夫示すことができた．さらに，例外処理に関する仕様，倉庫に対しての商品の搬入はコンテナ単位で行われ実装の正当性に関しても十分な記述をし，ESC/Java2るが，注文は品目単位で行われるため，コンテナの集において妥当であるとの出力を得られた．また，文合だけでなく，その中身をまとめた全品目の集合も倉献 [2] で議論されていた自明な例外を明示することの庫係に保持させた．全品目の集合とコンテナの集合中妥当性ついて，検証時間の観点から妥当性を示した．の内蔵品の合計は互いに矛盾しない．

2. 在庫管理プログラムの仕様
2. 1 概要3. 記 述 概 要
各クラスに対して invariant 節を用いた不変条件，在庫管理問題に対するクラス図は図 1 に表すように，また，各メソッドに対し requires 節，ensures 節を用“受付係”，“倉庫係”，“注文”，“顧客”，“品目”，“コいた事前，事後条件および，signals 節を用いて例外ンテナ” の 6 のクラスで表現できる．

が起こる条件，また確実に例外が起こり得ないことを受付係は ReceiptionDesk クラスで表され，外部か明示した．各クラスに対しての詳細な記述は，文献 [4]らの要求を受け取り，倉庫係に在庫が要求を満たすかを参照のこと．記述と検証作業に 2ヶ月ほどかかり，6

電子情報通信学会論文誌 X Vol. Jxx–X No. xx pp. 1–2 xxxx 年 xx 月

1

電子情報通信学会論文誌 xxxx/xx Vol. Jxx–X No. xx
表 1 仕様記述に対する検証時間
Table 1 Veriﬁcation time/∗@ public behavior
requires r != null;
requires checkStockSatisﬁed(r );assignable allitemlist, containerlist;
ensures (\sum ContainerItem i; \result.contains(i);((Item)i.getContainedItem().get(0)).getAmount())== r.getAmount();
ensures (\forall ContainerItem i; \result.contains(i);((Item)i.getContainedItem().get(0)).getName().equals(r.getName()));

10Class Name
ReceiptionDeskStorageContainerItem
RequestItem
Customer
Total

例外記述あり (s)
7.265
9.094
18.079
4.797
9.328
6.375
54.938

例外記述なし (s)
7.172
9.328
18.125
4.297
9.328
6.375
54.575@∗/図 2 倉庫の出庫処理の JML 記述 (メソッド記述は略)
Fig. 2 JML description of “Delivering order” in Storage class(without method body)

また，仕様記述において，\forall int i; 0 <= i && i < List.size();List.get(i)...のように，配列を扱うようにオブジェクトを参照した方が ESC/Java2 を通した検証にかかる時間が少な回のバージョン変更を行っている．
また，これらの JML 記述や Java プログラムの規模については約 1000 行 (内 JML は 400 行) であった.

3. 1 主要なメソッドに対する記述例
倉庫係における出庫処理の契約を図 2 に表す．r は受付係から送られてきた注文を表す．
まず，事前条件として注文 r が null でないこと，注文に対し在庫が十分あることが挙げられる．次に，assignable にてこのメソッドで更新され得る値を示す．
ここではコンテナリスト，全品目リストが更新される．
最初の ensures 節で示される事後条件は，戻り値で表わされる出庫指示書で，どのコンテナから品目をどれだけ出荷したかの合計が注文された数量と等しくなることを示している．ここでは一つの注文で一品目しか注文できない仕様のため，出庫指示書で示されたコンテナから取り出す品目の先頭に出庫される品目が存在するために get で先頭の要素を参照する．
二つ目の ensures 節で示される事後条件は，出庫指示書に書かれたすべてのコンテナから取り出した品目が要求された品目と等しいことを示している．

かった．実際に ContainerItem クラスの不変条件において適用した結果，配列形式にした場合について 18.1秒から 16.9 秒へと，1 秒程度の速度増加が得られた．
他のクラスについて同様の傾向があった．
この理由として，Simplify の入力となる論理式では，オブジェクトのフィールドを配列として表現するため [2]，配列を直接扱った方が定理証明の時間が少なくすむと考えられる．一方，仕様記述の観点からは前者の記述方のほうが好ましいと考えられる．

5. ま と め
酒屋の在庫管理問題についてモデル化し，JML を用いて仕様を記述することができた．また，Java プログラムを記述し，ESC/Java2 を用いた検証にも一分程度で成功することが確認できた．

JML が比較的詳細な設計を記述するための言語であることから，より抽象的な設計記述を JML に変換することを研究課題として考えている．具体的にはAlloy を用いた抽象段階での仕様の安全性が保証された設計から JML を自動生成することを考えている．
文

B.Meyer, Object-Oriented Software Construction,[2]

D.Cok,

4. ESC/Java2 による検証結果と考察
文献 [4] の JML 記述に対し，ESC/Java2 を用いてSecond Edition, Prentice Hall, 2000.

Workshop FTfJP’2004 Formal Techniques for Java-に対し Valid であるとの結果を得ることができた．各like Programs, Oslo, Norway, June 15, 2004. ICIS

クラスの検証にかかった時間を表 1 にまとめる．

report NIII-R0426, pp 41–48, 2004
[3]

二村良彦, 雨宮真人, 山崎利治, 淵一博, 新しいプログラミ
ング・パラダイムによる共通問題の設計, 情報処理学会会
誌 情報処理, Vol.26, No.5, pp.458–459, 1985.

[4]

尾鷲方志, 岡野浩三, 楠本真二, JML を用いた在庫管理プ
ログラムの設計と ESC/Java2 を用いた検証, 電子情報通信学会技術報告, Vol.107, No.176, pp.37-42, 2007.

証時間が目立って増加しているわけではないことが言える．これより，文献 [2] において言われた，例外が起こらない場合についてもそのことを明示すべきだ，という主張に対して，検証時間上のデメリットはないことを確認できた．
2

Reasoning with speciﬁcations containing

method calls in JML and ﬁrstorder provers, ECOOP

一部警告はあるものの，ほぼ全てのクラスのメソッド

上記の検証結果より，例外を明示することにより検献[1]（平成 xx 年 xx 月 xx 日受付）

Abstract In this letter, we designed and implemented the Warehouse management program in Javaand JML as a case study. This design has been veriﬁed with “ESC/Java2”. We report the lessons learnedin this process. Discussions about the issue on using JML in software development are also presented.
Key words ESC/Java2, JML, Warehouse Manaagement, Design and veriﬁcation, Design by Contract