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

信学技報
TECHNICAL REPORT OF IEICE.

OCL の JML への変換ツールの実装について
宮澤

清介†

岡野

浩三†

楠本

真二†

† 大阪大学大学院情報科学研究科〒 565–0871 大阪府吹田市山田丘 1–5
E-mail: †{k-miyazw,okano,kusumoto}@ist.osaka-u.ac.jp
あらまし OCL(Object Constraint Language) は UML 記述に対しさらに詳細に性質記述を行うために設計された言語である. 近年 MDA 関連技術の発展により，UML からプログラム言語への変換技術が着目をあびており，OCL から JML(Java Modelling Language) のようなプログラムレベルの仕様記述言語への変換技術も研究されつつある. 従来研究では OCL からの JML への変換についてコレクションに関するいくつかの重要な機能，とりわけ，iterate に非対応であった．研究グループではこの問題を，生成される Java スケルトンに対応するメソッドを記述するという方法で対応した．本稿ではその手法に基づき，OCL からの JML への変換ツールの実装について詳細に述べる．
キーワード

モデル変換，OCL，JML

On Implementation of a Translater from OCL into JML
Kiyoyuki MIYAZAWA† , Kozo OKANO† , and Shinji KUSUMOTO†† Graduate School of Information Science and Technology, Osaka University
Yamadaoka 1–5, Suita-Shi, Osaka, 565–0871 Japan
E-mail: †{k-miyazw,okano,kusumoto}@ist.osaka-u.ac.jp
Abstract OCL (Object Constraint Language) is an annotation language for UML, which can describe specification more precisely. In recent years, MDA techniques have emerged, thus translation techniques such as translationfrom OCL to JML (Java Modelling Language) as well as UML to some program languages, have gained a lot of
attention. Past researches on translation from OCL to JML often pays little attention to collection features, especially iteration. Our research group has proposed a method to overcome such the problem by using Java method
templates. In this report, we present an implementation of a tool of the translation based on the proposed method.
Key words model translation, OCL, JML

1. は じ め に

OCL から JML への変換については Hamie が文献 [8] において
構文変換技法に基づいた OCL から JML への変換法を提案しOCL(Object Constraint Language) [1] は UML 記述に対し，ており，Rodion と Alessandra らが文献 [9] において，Hamie

さらに詳細に性質記述を行うために設計された言語で，OMGの研究の拡張とツールの実装を示している．また，Avila らがによって標準化されている．

文献 [10] にて型の扱いなどについて改善を示しているものの，より実装に近い面での制約記述言語として，Java プログラム

いずれの方法も Collection の対応が不十分であり，iterate のに対して JML (Java Modeling Language) [2] が提案されてい対応が一部の演算に対応しているのみである．しかし，iterate

る．JML，OCL ともに DbC (Design by Contract) [3] の概念

はデータベースをモデル化する際など，広く用いられる演算でに基づきクラスやメソッドの仕様を与えることができる．

あるため，対応すべき問題だと考えられる．

近年 MDA(Model Driven Architecture) [4] 関連技術の発展

著者の所属する研究グループは，OCL 記述が付加されたクラにより，UML からプログラム言語への変換技術が注目をあびス図に対して，JML 記述への変換法を具体的に提示した [11]．

ている．UML クラス記述から Java スケルトンコードを自動

本稿では実装について詳しく述べる．

生成する方法についてはすでに既存研究で多くの方法が提案

以降，2 章で背景について述べ，3 章で文献 [11] で提案したされており [5], [6]，自動変換ツールも EMF フレームワークを手法について述べ，4 章で実装について述べ，5 章でまとめる．

用いた Eclipse プラグインなどの形で公開されている [7]．一方

—1—

2. 準

し評価されない.

備

文献 [11] では個々のループ演算に対応する Java メソッドを

本章では研究の背景となる諸技術と関連研究について簡単に触れる．

用意することでこの問題を解決することを提案した．iterate 演
算はデータベースをモデル化する際など，広く用いられる演算

2. 1 OCL

であるため，文献 [11] はこの演算の変換に対応するアルゴリズ

OCL(Object Constraint Language) は UML モデルに対し，ムを示したという点で有用である．しかし，文献 [11] では具体さらに詳細に性質記述を行うために設計された言語であり，的な実装方法までは示しておらず，生成される JML が実用的

UML と同様に OMG によって標準化されている．UML では，なものであるかといった評価がなされていない．

実装時にモデルがどのように開発されるべきか，といった詳細

本稿では変換に際し型情報を用いた，より厳密な変換プロセ

な情報を表すことができない．このような問題を解決するため，スを提案し，そのプロセスを用いて UML や OCL の入力部分

OCL が導入された．

から，JML を付加した Java コードを出力する部分までをツールとして実装することにより，利用者に利便性も与える．

2. 2 JML
JML(Java Modeling Language) は，Java のメソッドやオブ

3. iterate 演算の変換方法

ジェクトに対して制約を記述する言語である。記述においてはJava の文法を踏襲し，初心者でも記述しやすい特徴を持つ．まこの章では文献 [11] で提案した iterate 演算の変換方法についた，記述は Java コメント中に記述できるため，プログラムのて述べる．この変換方法は文献 [8], [9] の構文変換で未対応であ実装，コンパイルや実行に影響がない．

る，iterate 演算のについて対応している．そして，Collection

JML には，コード実行時に JML 記述に違反しないかをチェックするランタイムアサーションチェッカや，JUnit 用のテスト
ケースのスケルトンやテストメソッドを自動で出力する JM-

LUnit [13]，JML 記述に対する Java プログラムの実装の正しさをメソッド単位で静的検査できる ESC/Java2 など，コードの一部の演算を，iterate 演算を用いた式で表現することで，

OCL-JML 変換の妥当性を向上させる方法について述べる．
3. 1 iterate 演算の変換
iterate 演算の変換は次の理由により，単純な構文変換では対応できない．

•の検証を効率化するための様々なツールがサポートされている．

iterate 演算の引数はほぼ任意の OCL 式であり，単純な2. 3 関 連 研 究

構文変換をするためには，変換先の言語 L において，L の任意

UML から JML への変換については，Engels らの文献 [5] や式の動的な評価機構が必要となる．

•

Harrison らの文献 [6] 等において言及されているが，変換する上で，UML 上での仕様の厳密な定義を行う OCL に関する言JML や Java1.6 はそのような機構を直接的にはサポートしていない．

及が不十分である．Hamie は文献 [8] において構文変換技法に

本研究では，iterate 演算に引数として与えられる OCL 式を基づいた OCL から JML への変換法を提案している．Rodion

評価するメソッドを変換時に作成し，JML 式でそのメソッドのと Alessandra らは文献 [8] を基に，文献 [9] において未対応で戻り値を参照することで，間接的にこの問題に対応する．具体

あった Tuple 型や Collection 型の演算の一部に関する変換法

的には，µ(c1 −>iterate(e; init | body)) に対し，初期化式 initを提案し，ツールの実装を示している．Avila らは文献 [10] にで T1 型の変数 res が初期化され，Collection のすべての要素

おいて，文献 [8] においてマッピングされた OCL と JML のe に対して body を実行した評価結果が res に入る．この演算Collection 型の差異を吸収し，より完全な変換を行うライブラに対し，図 1 のメソッドを生成する．ここで，µ() は引数の式リを提案し，変換後の可読性について言及している．しかしな

を Java 構文に変換する関数を表す．

がら，いずれの方法も Collection ループ演算の中で最も基本的な演算である iterate 演算への対応が不十分である．iterate 演
算は，引数で与えられた式を Collection のすべての要素に対して繰り返し実行するという演算である．また，iterate 演算の引変換例を以下に示す．以下の OCL 式 からメソッドを生成することを考える．

c−> iterate(e; acc: Integer = 0 |if e = ‘ocl′ then acc + 1 else acc endif)

数として与えられる OCL 式について，具体例として，式（1）のような演算がある．これはコレクション students から score(2)

図 1 の init と body に OCL 式（2）の対応する部分を当てはが 70 以上の要素を抽出したコレクションを返す演算である．

students−> select(score > 70)(1)

private T1 mPrivateUseForJML01() {µ(init);JML や Java において score > 70 といった式の動的な評

for (T2 e: µ(c1 )){価機構が用意されておらず直接対応することができないとい

res = µ(body)}

う問題点もある．例えば，式（1）に対し，対応する Java メ

return res;

ソッド select(exp) を用意した場合，OCL 式で与えられる引数}

score > 70 が exp として与えられることになり，select の評価

図 1 iterate メソッド

時の 1 回しか評価されず，以降、ループのたびに動的に繰り返Fig. 1 iterate method—2—めると，図 2 のようになる．
このメソッドに，µ 変換を適用することで，図 3 のメソッドが生成される．

iterate 演算を含む JML 式は，例として図 4 のように与えら

表 1 Collection-Iterate 対応表

Table 1 correspondence table of the collection and iterationc1 −>exists(a1 | a2 )= c1 −>iterate(c1 −>forAll(a1 | a2 )= c1 −>iterate(c1 −>count(a1 )= c1 −>iterate(

a1 ; res : Boolean = false | res or a2 )れる．

a1 ; res : Boolean = true | res and a2 )3. 2 Collection 演算の変換

e; acc : Integer = 0 |この節では，Collection 演算の一部を iterate 演算を用いた式に変換することについて述べる．iterate 演算を用いて表現でき

if e = a1 then acc + 1 else acc endif)
c1 −>isUnique(a1 | a2 ) = c1 −>collect(a1 |Tuple {iter=Tuple{a1 }, value=a2 } ) −>る Collection 演算の一部を表 1 に示す．これらの表現は OCL

forAll(x, y | (x.iter <> y.iter)の定義書 [1] で定義されているため，OCL-JML 変換の妥当性
を OCL 定義書に委ねることができるという点が利点である．
一方欠点としては，iterate に対応するためのメソッドが多く挿入され，JML はそのメソッドをそれぞれ参照するため，Java

implies x.value <> y.value)c1 −>any(a1 | a2 )= c1 −>select( a1 | a2 )−>asSequence()−>ﬁrst()

c1 −>one(a1 | a2 )= c1 −>select( a1 | a2 )−>size()= 1

c1 −>collect(a1 | a2 )= c1 −>collectNested( a1 | a2 )−>ﬂatten()

変換された JML 式の読解性が低下することが挙げられる．この問題の解決としては変換ツール実装時に，Collection 演算を

iterate を用いて表現する場合としない場合の両方の変換に対応できるようにすることが考えられる．

4. 実

装

本章では実装に関して詳細に述べる．図 5 にツールの概要を示す．このツールは最終的に Eclipse のプラグインとして開発することを考えている．

4. 1 UML から Java への変換
UML クラス図から Java ソースコードに変換する方法に関しては，Eclipse UML Studio Edition を利用する．このツールを選定した理由として，属性に対する型の割り当てや関連に

private int mPrivateUseForJML01() {µ(acc : Integer = 0);
for (String e : c){acc = µ( if e = ‘ocl’ then acc + 1 else acc endif)}
return acc;}
図 2 init と body に式を割り当て

Fig. 2 assignment of the OCL expression into init and body
図5

ツール全体図Fig. 5 Tool Overview

private int mPrivateUseForJML01() {int acc = 0;
for (String e : c){acc=(e.equals(“ocl”)? acc + 1: acc) };return acc;

関する設定などを詳細に記述することができる点や，出力される XMI ファイルの構造がコンテキスト情報の抽出に適している点などが挙げられる．

}

UML から得られるコンテキスト情報から，以下の情報を利図 3 Java 変換後の iterate メソッド

用する．

Fig. 3 iterate method after Java translation

•

クラス名

•

属性名

•

属性の型

•

操作名

•

操作の引数の型•

操作の戻り値の型

mPrivateUseForJML01()> 0
図 4 iterate メソッドの JML からの呼び出し

Fig. 4 the call of iterate method from JML expression

—3—

•

関連端名

とする演算であることを表すフラグ•

多重度

また，UML のコンテキスト情報を得るために，ANTLR パー•

継承しているクラス

サを拡張して UML 情報が記述された XMI ファイルを入力で4. 2. 2 節で詳細に述べるが，OCL から JML へ変換するためきるようにする．XMI ファイルから，属性・操作名をキーとしの情報として，変数や演算結果の型の情報が必要になる．OCLてその型名を返す Map を作成し，OCL 構文内に属性・操作名の構文では属性や操作の参照は非常に頻繁に起こるため，それが現れたとき，Map から型を取得する．

らの名前と型をコンテキスト情報として必要とするのは自明でCollection 型の演算には count(),size(),isEmpty() など，様々ある．変数や，操作の戻り値の型はユーザが定義した型であるな演算が OCL の標準で与えられているが，この型推論も，ユー

場合があり得るので，クラス名の情報も必要になる．生成されザ定義の操作名から型情報を得る方法と同様に，演算名をキーた JML をより正確なものにするため，操作の引数の型も与えとしてその型名を返す Map で解決することを考えている．

ておくことで，OCL 構文解析の段階で型不整合は検出しておまた，UML や JML では数値を表す型として byte, short,

きたい．また，関連しているクラスの情報を用いた演算も頻繁

char, int, long, float, double といった型が定義されているが，に利用される．そのためには関連端名が必要である．誘導の型

OCL では Integer 型と Real 型の 2 種類のみしか定義されていは，ユーザ定義型もしくはユーザ定義型のコレクションのいずない．Integer, Real の両型とも，上限は定義されていないため，れかである．その型は多重度によって決まるため，多重度の情

本稿では Integer 型は int 型に，Real 型は double 型に対応さ報が必要となる．関連クラスは，あるクラスのサブクラスであせることとする．設計の自由度に制限を与えないため，OCL でる可能性があり，スーパークラスの属性や操作を利用するためは対応していない long や float などの型推論も，評価可能にすには，継承クラス情報が必要になる．以上により，UML からる．演算による型の評価は，JML のものと統一する．例えば，利用するコンテキスト情報の必要性を述べた．UML には他にbyte + short の評価型は int，long ∗ f loat の評価型は float な

可視化の情報も含まれるが，操作の多用で OCL を複雑にさせどである．co また，ここで OclVoid 型の扱いについて述べる．

ないため，利用はしない．

OclVoid 型は未定義値である Undefined 定数のみをもつクラス

文献 [9] では UML クラス図描画ツールに Violet [14] が用いである．Undefined はオブジェクトがサポートしていない型にられているが，Violet は UML の作図を簡単な操作で素早く実キャストしたり，空のコレクションから要素を取得しようとす

現することに特化しており，属性の型を定義するなどの詳細なると戻り値として得られる値である．これは JML では null と情報を持たせることができない．このため，出力される XMI

して扱われるが，null との違う点として，True or Undefined

ファイルも厳密に定義されたものではないので，属性や関連ななどの一部の論理演算においては，OclVoid は式そのものを未

どの情報取得が困難だと考え，本研究では新たにツールの選定

定義としては扱わず，正当な評価（上記の場合は True）を返すを実施した．

というものがある．この点に関しては，OCL の構文解析器に4. 2 OCL から JML への変換

動的な評価機構を持たせられないため，JML に出力する際に4. 2. 1 OCL 構文解析器の実装

工夫を施す必要がある．そのために，OCL 抽象構文木のノーOCL 構文解析器の実装には，ANTLR を利用する．ANTLR

ドに flag を持たせる．詳細は 4. 2. 5 節で述べる．

は LL(k) 構文解析を用いた構文解析器自動生成ツールである．

ユーザ定義型の型推論に関しては，OCL の定義書に従い，構文解析器の出力言語として Java をサポートしており，構文‘=’,‘<>’, oclIsUndefined(), oclIsKindOf(), oclIsTypeOf(),

解析器と同時に字句解析器も出力することから，ツール開発のoclIsNew(), oslAsType(), oclInState() に対応する．

速度を向上させることができる．

OCL 定義書で定義されている OCL 構文からは型的に不整合

4. 2. 2 型 推 論な表現式が導出され得るが，そのような型不整合な式は Java やこの節では，構文解析器に型情報を付加することについて

JML で直接扱えないため，例外を出力し，コンパイルエラー

述べる．二つのオブジェクトが同値であることを評価する演になるようにする．

算に関して，OCL では任意の型において ‘=’ が用いられるが，4. 2. 3 Collection 演算の iterate 演算への変換

JML では基本データ型の比較には ‘==’ が用いられ，参照型に

3. 2 節で述べたように，一部の Collection 演算を iterate 演

は equals() メソッドが用いられる．変換を正しく実行するため算に変換する方法について述べる．対応方法としては，各演算には，構文木のノードが変数や演算の型を保持しなければならを iterate 演算で表現した構文木をテンプレートとして与えてない．

おき，ノードのリンクを変更するなどの方法を考えている．具ANTLR パーサが出力する OCL 抽象構文木のノードは型情体例として， c −>count(′ ocl′ ) を iterate 演算を用いた構文木

報を持たないので，ノードクラスを拡張することで対応した．

に変換することを考える．count 演算を iterate 演算を用いた式

拡張したノードは，以下の 3 つの情報を持つこととする．

で表すと，c1 −>iterate( e; acc : Integer = 0 | if e = a1 then•token: 演算子，feature 名，終端 token 値など

acc + 1 else acc endif) で表される．構文木テンプレートは図•

type: 該当ノードの部分木に対する型

6 のように与えられる．

•

children: 子ノードリスト•

flag: 部分木が関連もしくは，コレクション型を戻り値

このテンプレートに対し，e に当てはまる型名と a1 に当て
はまる OCL 抽象構文木を入力することで，テンプレート内の—4—

表 4 Collection 演算の µ 変換表

Table 4 µ translation table of the operation of the collection typeµ(c1 −>size())= µ(c1 ).size()µ(c1 −>includes(a1 ))= µ(c1 ).has(µ(a1 ))µ(c1 −>isEmpty())= µ(c1 ).isEmpty()µ(c1 −>notEmpty())= !µ(c1 ).isEmpty()µ(c1 −>excludes(a1 )) = µ(c1 −>count(a1 ) = 0)µ(c1 −>count(a1 ))= µ(c1 −>iterate( e; acc : Integer = 0 |if e = a1 then acc + 1 else acc endif))

図 6 count 演算の構文木テンプレート

Fig. 6 The tree template of count operation•

flag: 部分木が関連もしくは，コレクション型を戻り値とする演算であることを表すフラグ

feature 情報を用いて，JML を文字列化する際に文字列を出力する順序を制御する（詳細は 4. 2. 5 節で述べる）．

flag は 4. 2. 2 節で述べた，undefined を用いた論理演算の差異を吸収するために用いる（詳細は 4. 2. 5 節で述べる）．
具体的な JML 抽象構文木の例として，コンテキスト宣言を
図 7 count 演算を iterate 変換した結果

Fig. 7 The result of translation from count operation to iterate含む構文木，iterate 演算を含む構文木に対して，それぞれ図 8,9 でその構成を示す．
4. 2. 5 JML-Text トランスレータ

operation

この節では，OCL-JML 変換によって得られた JML 抽象構
ノードを変更することを考えている．この場合，型名に String，′′

文木を入力とし，構文木をテキストとして出力する方法についOCL 構文木に ocl の構文木を与える．テンプレートに情報をて述べる．まず，JML トランスレータクラスは以下のデータ構与えて出力される OCL 抽象構文木は図 7 で表される．

造を持つクラスのリストを，フィールドとして持つこととする．

4. 2. 4 OCL-JML 変換アルゴリズム•

className : 制約を加える対象となるクラス名

以下の変換規則に従って，OCL 抽象構文木を葉に近いノー•

methodName : 制約を加える対象となるメソッド名

ドから順に，JML 抽象構文木へと変換する．文献 [8] の記法に•

jmlText : 挿入する JML 式のテキスト

従い，OCL 式から JML 式への変換関数の表記を µ で与える．

•

iterateMethod : 文字列化した iterate メソッドのリスト

スペースの都合上，変換規則の一部を掲載する（表 2，3，4）．

まず図 8 のコンテキスト情報から JML 文を挿入するべきクラai は Integer, Real, Boolean の任意の型，ci は Collection 型の任意の型を表している．
ここで，変換する JML の構文木の構成について述べる．構
文木の各ノードには以下の情報を持たせることを考えている．

•

token: 演算子，feature 名など•

feature: ノードの種類•

children: 子ノードリスト
表 2 数値型の µ 変換表

Table 2 µ translation table of the numeric typeµ(a1 = a2 )= µ(a1 ) == µ(a2 )図 8 コンテキスト宣言を含む JML 抽象構文木µ(a1 > a2 )= µ(a1 ) > µ(a2 )Fig. 8 JML ABST Tree containing context declarationµ(a1 < a2 )= µ(a1 ) < µ(a2 )µ(a1 >= a2 ) = µ(a1 ) >= µ(a2 )µ(a1 <= a2 ) = µ(a1 ) <= µ(a2 )µ(a1 <> a2 ) = µ(a1 )! = µ(a2 )表 3 Collection 型の µ 変換表

Table 3 µ translation table of the collection typeµ(c1 = c2 )= µ(c1 ).equals(µ(c2 ))µ(c1 > c2 )= µ(c1 ).containsAll(µ(c2 ))&&!µ(c1 ).equals(µ(c2 ))µ(c1 < c2 )= µ(c2 ).containsAll(µ(c1 ))&&!µ(c1 ).equals(µ(c2 ))µ(c1 >= c2 ) = µ(c1 ).containsAll(µ(c2 ))µ(c1 <= c2 ) = µ(c2 ).containsAll(µ(c1 ))µ(c1 <> c2 ) = !µ(c1 ).equals(µ(c2 ))図 9 iterate 演算を含む JML 抽象構文木

Fig. 9 JML ABST Tree containing iterate operation—5—

"public" + type of a return value+ "mPrivateUseForJML01(){ \n"ことと，MDA へ適用することの 2 点を考えている．ツールの評価に関しては，実用的な制約記述に対し実時間で変換できる
か，与えた OCL 式に対して JML のランタイムアサーション+ "\t" + init + ";\n"+ "\t for(" + type of e + " e :"+ collection name "){\n"+ "\t\t" + name of return variable "="+ body + "}\n"+ "\t return" + name of return variable + ";}"

チェッカが意図した結果を返すかどうかなどの評価を行うことを考えている．一方，MDA への適用では MOF と QVT を用いたモデル変換手法への適用も考えている．これは UML/OCLのメタモデルと，Java/JML のメタモデルのマッピングを定義することでモデル変換を実現する手法である．
謝辞

図 10 iterateMethod に格納するテキスト

Fig. 10 generation text of iterate method

スとメソッド名を取得し，それぞれ className と methodNameに格納する．次に，JML の部分木を以下の方法に従い文字列化し，jmlText に格納する．

iterate 演算を用いた構文は，jmlText 用には mPrivateUseForJML() を出力し，iterateMethod に図 10 のように生成したテキストを追加する．

4. 2. 2 節で述べた Undefined を用いた論理演算への対応であるが，flag を用いて解決する．例えば，焦点を当てているノードの種類が ‘or’ であり，その右の子の flag が True であったとき，or 演算の式が True or Undefined である可能性がある．この条件を満たす場合，JML-Text トランスレータは論理式の右辺として以下のコードを出力する．

(a_1 == null ? false :throw new JMLTranslationException())
左辺の boolean の評価値により，or 演算の評価値に影響を与えないため，右辺が null であった場合は false を返す．null でな
い場合は or 演算の型不整合であるので，検証時に例外を出力するようにしている．

4. 3 Java と JML の統合
この節では，Java と JML の統合を行う（図 5 の Synthesizerに相当する）モジュールの実装について述べる．
まず，className を用いて JML を挿入する Java ファイルを決定する．methodName が null(挿入する制約式が不変条件)の場合，クラス宣言の 1 行下に jmlText を挿入する．method-

Name が null でない（挿入する制約式が事前条件または事後条件）場合，methodName を参照して JML を挿入するメソッド
を特定し，メソッド宣言文の 1 行上に jmlText を挿入する．
最後に，Java ファイルの一番後ろに iterateMethod の要素をすべて挿入する．

5. あ と が き

本研究の一部は科学研究費補助金基盤 C（21500036）と文部科学省「次世代 IT 基盤構築のための研究開発」（研究開
発領域名：ソフトウェア構築状況の可視化技術の普及）の助成
による．
文

献

[1] O. M. Group: “Ocl 2.0 speciﬁcation” (2006). http://www.
omg.org/cgi-bin/apps/doc?formal/06-05-01.pdf.
[2] G. Leavens, A. Baker and C. Ruby: “Jml: A notation for detailed design”, Behavioral Speciﬁcations of Businesses andSystems, pp. 175–188 (1999).
[3] B. Meyer: “Eiﬀel: the language”, Prentice-Hall, Inc., Upper
Saddle River, NJ (1992).
[4] A. Kleppe, J. Warmer and W. Bast: “MDA explained: themodel driven architecture: practice and promise”, AddisonWesley Longman Publishing Co., Inc. Boston, MA, USA(2003).
[5] G. Engels, R. Hücking, S. Sauer and A. Wagner: “Umlcollaboration diagrams and their transformation to java”,
UML1999 -Beyond the Standard, Second International Conference, pp. 473–488 (1999).
[6] W. Harrison, C. Barton and M. Raghavachari: “Mapping
uml designs to java”, Proc. of the 15th ACM SIGPLAN
conference on Object-oriented programming, systems, languages, and applications, pp. 178–187 (2000).
[7] Eclipse Foundation: “Eclipse modeling framework”. http://www.eclipse.org/modeling/emf/.
[8] A. Hamie: “Translating the object constraint language into
the java modelling language”, In Proc. of the 2004 ACM
symposium on Applied computing, pp. 1531–1535 (2004).
[9] M. Rodion and R. Alessandra: “Implementing an ocl to jml
translation tool”, 電子情報通信学会技術研究報告, 第 106 巻,
pp. 13–17 (2006).
[10] C. Avila, G. Flores, Jr. and Y. Cheon: “A library-based
approach to translating ocl constraints to jml assersions forruntime checking”, International Conference on Softw. Eng.
Research and Practice, pp. 403–408 (2008).
[11] 尾鷲, 岡野, 楠本：“メソッドの自動生成を用いた ocl の jml への変換”, コンピュータ ソフトウェア, 27, 2, pp. 106–111 (2010).
[12] J. Specs: “Samples of jml speciﬁcations”. http://www.
eecs.ucf.edu/∼leavens/JML/examples.shtml.
[13] Y. Cheon and G. Leavens: “A simple and practical approach to unit testing: The jml and junit way”, ECOOP
2002 Object-Oriented Programming, pp. 1789–1901 (2006).
[14] A. de Pellegrin: “Violet. uml modeling tool” (2007). http://www.horstmann.com/violet/.

本稿では著者の所属する研究グループが提案する，OCL 記
述を JML 記述へと変換する手法を紹介し，とりわけ iterate 演算の変換に対する手法を紹介することで，従来手法で提案されていたクラスより広いクラスに対して適用できることを示した．
本研究ではその手法に対し，型推論や OCL-JML 変換表など具体的な実装方法を示した．
今後の課題としては，本ツールを完成させて評価実験を行う—6—