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

信学技報
TECHNICAL REPORT OF IEICE.

制約記述言語 OCL と JML のモデル駆動開発技法に基づいた
双方向の変換手法の提案
榛葉浩章†

花田健太郎†

岡野 浩三†

楠本真二†† 大阪大学大学院情報科学研究科〒 565–0871 大阪府吹田市山田丘 1–5
E-mail: †h-shimba@ics.es.osaka-u.ac.jp, ††{k-hanada,okano,kusumoto}@ist.osaka-u.ac.jp
あらまし

OCL (Object Constraint Language) は UML 記述に対しさらに詳細に性質記述を行うために設計された言語である. 近年 MDA 関連技術の発展により，UML からプログラム言語への変換技術が着目を浴びており，OCL からJML (Java Modelling Language) のような プログラムレベルの仕様記述言語への変換技術も研究されつつある. 研究グ
ループでは，OCL から JML への変換及び，その逆変換である JML から OCL への変換について研究しており，双方向の変換を実現することで，仕様記述レベルでのラウンドトリップエンジニアリングによる開発の支援や，様々な制約
記述言語間での相互変換を実現していきたいと考えている．本稿では，モデル変換的手法に基づいた OCL から JML
及び，JML から OCL への変換ツールの試作型の実装について述べる．
キーワード

OCL，JML，RTE，モデル変換

Bi-directinal Translation Method between OCL and JML
based on Model Driven Development
Hiroaki SHINBA† , Kentaro HANADA† , 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: †h-shimba@ics.es.osaka-u.ac.jp, ††{k-hanada,okano,kusumoto}@ist.osaka-u.ac.jp
Abstract OCL (Object Constraint Language) is an annotation language for UML, which can describe specication more precisely.In recent years, MDA based techniques have emerged, thus translation techniques such as translation from OCL to JML(Java Modelling Language) as well as UML to some program languages, have gained a lot of attention.Our research grouphas been studying not only a translation method from OCL to JML but also a translation method from JML to OCL.By implementing bi-directional translation between OCL and JML, we can support the following two items.One is development by
round trip engineering at the design level.The other one is translations among various formal specification languages.In thisreport, we present two implementations based on model translation techniques.Translations from OCL to JML and from JML
to OCL.
Key words OCL，JML，RTE，Model Translation

1. は じ め に(Java Modeling Language) [5] への変換技術も研究が行われている．OCL は UML 記述に対し，さらに詳細に性質記述を行う

近年 MDA (Model Driven Architecture) [1] 関連技術の発展にために設計された言語で，OMG (Object Management Group) により，UML (Unified Modelling Language) からプログラム言語

よって標準化されている．より実装に近い面での制約記述言への変換技術が注目を浴びている．UML クラス記述から Java語として，Java プログラムに対して JML が提案されている．

スケルトンコードを自動生成する方法についてはすでに既存

JML，OCL ともに DbC (Design by Contract) [6] の概念に基づき研究で多くの方法が提案されており [2], [3], 自動変換ツールもクラスやメソッドの仕様を与えることができる．

EMF フレームワークを用いた Eclipse プラグインなどの形で公過去に著者の所属する研究グループは，OCL 記述が付加さ開されている．OCL (Object Constraint Language) [4] から JML

れたクラス図に対して，JML 記述への変換法を具体的に提示—1—

し [7]，文献 [8] において実装を示している．しかし，既存ツーられる．これらは，MDA におけるモデル変換である．

ルは MDA の主流であるモデル変換的な実装ではなく，抽象構

モデル変換にはモデルからモデルへの変換である

文木を介したマッピングで実装されている．現在では OCL かModel2Model 変換 (M2M)，モデルからコードへの変換であら JML 以外の複数の言語への変換の実現を目標としているが，る Model2Text(M2T) が存在する．M2T 変換機能を提供する

既存手法ではそれぞれの変換を独立に実装する形になるため実ツールとして，UML2Java [15] などが挙げられる．

装の再利用性が低く，複数言語への変換の実装には向かない．

2. 4 RTE

また，既存の実装は変換の達成を主な目的としており，ツール

RTE (Round Trip Engineering) とは，フォワードエンジニアリ

そのもののユーザビリティは低い．

ングとリバースエンジニアリングを反復しながら，モデルとソー

本稿では，Xtext [9] を用いて OCL が付加された UML クラス

スコードを徐々に詳細化していくことで開発を行う手法であり，図の構文定義を行い，その構文定義から JML が付加された Java

機能の変更や要求の変更に強いという特徴を持つ．[10], [11] IDEのスケルトンコードへの変換を定義する方法での実装を試みた．

等の RTE 開発支援ツールを用い，設計・コードのいずれかの変

Xtext では構文定義と変換部分が独立しており，構文定義の再更の一部を他方に自動的に反映していくものが一般的である．

利用性が高いことが利点として挙げられる．また，構文定義に

RTE を行う際には，モデルとソースコードの整合性を保つ必要対応した高機能なエディタを生成することができるため，ツー性があるが，自動的に整合性を保つ様々なツールが存在する．

ルそのもののユーザビリティの向上も見込めると考えられる．

2. 5 Xtext

また，仕様記述レベルでのラウンドトリップエンジニアリン

Xtext [9] とは，モデルの構文定義や，構文定義に従ったモデ

グ (以下，RTE) [10], [11] による開発の支援，様々な制約記述言ルからテキストへの変換ルールの構築などをサポートするた

語間での相互変換を目的として，OCL から JML への変換と同めのフレームワークである．モデルの構文定義を行うことで，様の方法で，JML から OCL への変換を試みた．RTE とは，フォコード補完機能やエラー検出機能などを備えたエディタを生成

ワードエンジニアリングと，リバースエンジニアリングを反復することができる．生成されたエディタ上で入力となるテキス

しながら，モデルとソースコードを徐々に詳細化していくこと

ト型モデルを記述すると，自動的に変換ルールを用いてモデルで開発を行う手法であり，OCL と UML，JML と Java のスケをテキストに M2T 変換する．

ルトンコードを徐々に詳細化していく形で仕様記述レベルでの開発を支援していきたいと考えている．
以降，2 章で背景について述べ，3 章で実装について述べ，4
章で評価について述べ，5 章でまとめる．

2. 準

備

本章では，背景知識や関連研究などについて簡単に触れる．

2. 1 OCL
OCL (Object Constraint Language) は UML モデルに対し，さ2. 6 関 連 研 究研究グループでは，OCL から JML への変換に関する多くの既存研究 [16] [17] において非対応だった iterate 演算に対応した変換手法の提案・実装を行っている [8]．例えば，式 (1) のような iterate の演算が与えられた場合，この演算に対応した Java のメソッドを生成し，JML 側から呼び出すことで変換を実現している．

Set{1, 2, 3}−> iterate(i : Integer;
sum : Interger = 0 | sum + i)

らに詳細に性質記述を行うために設計された言語であり，UMLと同様に OMG によって標準化されている．UML では，実装時(1)

具体的には，式 (1) に対応するメソッドは図 1 となる．

にモデルがどのように開発されるべきか，といった詳細な情報を表すことができない．このような問題を解決するため，OCL

private int mPrivateUseForJML01(){が導入された．

int sum = 0;
for (int i : set){

2. 2 JML

sum = sum + i;

JML (Java Modeling Language) は，Java のメソッドやオブジェ}

クトに対して制約を記述する言語である．記述においては Javaの文法を踏襲し，初心者でも記述しやすい特徴を持つ．また，
記述は Java コメント中に記述できるため，プログラムの実装，

return sum;}

図 1 iterate 演算を変換したメソッドの例

コンパイルや実行に影響がない．

JML には，コード実行時に JML 記述に違反しないかをチェッ

しかし，既存ツールは MDA の主流であるモデル変換的な実クするランタイムアサーションチェッカや，JUnit 用のテスト装ではなく，抽象構文木を介したマッピングで実装されている．

ケースのスケルトンやテストメソッドを自動で出力する JMLU-

今後 OCL から JML 以外の複数の言語への変換の実現を目標と

nit [12]，JML 記述に対する Java プログラムの実装の正しさをしているが，既存手法ではそれぞれの変換を独立に実装する形

メソッド単位で静的検査できる ESC/Java2 など，コードの検証になるため実装の再利用性が低く，複数言語への変換の実装にを効率化するための様々なツールがサポートされている．

は向かない．また，既存の実装は変換の達成を主な目的として

2. 3 モデル変換
代表的なモデル変換として QVT [13] や ATL [14] などが挙げ

おり，ツールそのもののユーザビリティは低い．
また，要求変更に対して RTE による開発を実施することで，—2—

3. 2. 2 OCL から JML への変換ルールの定義
表 1 に変換ルールの一部を記載する．OCL 式から JML 式への変換関数の表記を µ で与え，ai は Integer, Real, Boolean の任
意の型，ci は Collection 型の任意の型を表している．
表 1 OCL から JML への µ 変換表の一部

ションを対象に RTE を支援するための研究などが存在している [18]．

= µ(a1 ) <= µ(a2 )µ(a1 <> a2 )= µ(a1 )! = µ(a2 )µ(c1 −>size())= µ(c1 ).size()µ(c1 −>isEmpty())= µ(c1 ).isEmpty()

OCL-JML 間の変換は既存研究とほぼ同様に定義している [8]．
exists 演算や forall 演算のようなコレクションループは表 2 のように iterate 演算に置き換えることが可能なため，既存研究で本稿では，Xtext を用いて OCL が付加された UML クラス図の構文定義を行い，その構文定義から JML が付加された Javaのスケルトンコードへの変換を定義する方法で実装することで，研究グループの既存ツールの課題点を改善することを試みた．

3. 実= µ(a1 ) == µ(a2 )µ(a1 <= a2 )µ(c1 −>includes(a1 )) = µ(c1 ).has(µ(a1 ))図 2 Xtext による実装概要

開発期間を短縮し，効率化することができる．Web アプリケーµ(a1 = a2 )装は iterate 演算以外のコレクションループも iterate 演算に置き換
え，その OCL 式と意味的に等価なメソッドを生成して，その値を JML 側から参照する方法で変換していた．しかし，この変換方法ではコードの可読性が低下するといった問題点が挙げられていたため，本稿の実装では JML にメソッドが存在している exists 演算や forall 演算などは直接的にマッピングを行っ

この章では，実装に関して述べる．

ている．

3. 1 実 装 方 針
Xtext を用いて，モデルの構文定義を行い，モデルの構文定
義からコードへの変換ルールを定義することでそれぞれの変換を実現する．図 2 に実装の概要を示す．

表 2 Collection-Iterate 対応表の一部
c1 −>exists(a1 | a2 )= c1 −>iterate(c1 −>forAll(a1 | a2 )= c1 −>iterate(

a1 ; res : Boolean = false | res or a2 )a1 ; res : Boolean = true | res and a2 )この実装方法には以下のような利点が挙げられる．

•

モデルの構文定義は，テキストへの変換ルールの実装か

ら独立しているため構文定義そのものの再利用性が高い．

•

Xtext ではモデルの構文定義を行うことで，コード補完

や文法エラーの検出を行えるユーザビリティの高いエディタが得られる．

3. 2 OCL から JML への変換

st1 −>select(a1 | a2 )) = st1 −>iterate( a1 ; res : Set(T ) = Set {} |if a2 then res −>includeing (a1 ) else res endif)
st1 −>reject(a1 | a2 ))= st1 −>select( a1 | not a2 )また，DSL に従ったモデルの例を図 3 に，モデルからの変換
結果を図 4 に例として示す．

ここでは，OCL から JML への変換の実装について述べる．

3. 2. 1 OCL が付加された UML の構文定義
OCL を付加できる UML クラス図のモデルの構文定義を行った．UML の部分に関しては，Xtext で既存のものが存在するの
図 3 DSL に従ったモデルで流用し，OCL 部分を追加する形で構文定義を行った．OCL
部分に関しては，メソッド名や引数の数，戻り値の型などの場
合分けを特に考慮した．変換ルールの作成は構文定義に依存するので，構文定義の段階で詳細な場合分けを行うことで意味的な解析にかかるコストが削減され，構文定義を再利用することの有用性が高まると考えられる．また，生成されるエディタのエラー検出やコンテンツアシストは構文定義に依存するので，構文定義の段階で場合分けを厳密に定義するほどコンテンツア
シスト機能などが充実したエディタが得られる．これらのことから，メソッド名なども考慮した構文定義を行うことは，ユーザビリティの観点や実装の再利用性の観点から有用であると考
えられる．
図4

モデルから変換された出力結果—3—

3. 2. 3 Oclvoid 型の扱いについて
OclVoid 型は未定義値である Undefined 定数のみをもつクラスである．Undefined はオブジェクトがサポートしていない型にキャストしたり，空のコレクションから要素を取得しようとすると戻り値として得られる値である．これは JML では null

表 3 µ 変換ルールµ(b1 ?b2 :b3 )= if µ(b1 ) then µ(b2 ) else µ(b3 ) endifµ(b1 <==>b2 )= µ(b1 )= µ(b2 )µ(b1 <=! =>b2 )= µ(b1 ) <> µ(b2 )µ(b1 ==>b2 )= µ(b1 ) implies µ(b2 )µ(b1 <==b2 )= µ(b2 ) implies µ(b1 )として扱われるので，ほとんどの変換においては null としてµ(b1 &&b2 )= µ(b1 ) and µ(b2 )扱っている．

µ(b1 ||b2 )= µ(b1 ) or µ(b2 )µ(b1 |b2 )= µ(b1 ) or µ(b2 )null との違う点として，例えば True or Undefined などの一部の論理演算においては，OclVoid は式そのものを未定義としてµ(b1 ˆb2 )= µ(b1 xor µ(b)は扱わず，正当な評価（上記の場合は True）を返すというものµ(b1 & b2 )= µ(b1 ) and µ(b2 )がある．これに対応するためには，Undefined をこの場合は単純に null として扱うのではなく，以下のように扱えば対応できる．

(a_1 == null ? false :µ(\result)= resultµ(\old(a1 ))= µ(a1 )@preµ(\not modified(a1 )) = µ(a1 ) = µ(a1 )@preµ(\fresh(a1 ))= µ(a1 ).oclIsNew()

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

3. 3 JML から OCL への変換
ここでは JML から OCL への変換の実装について述べる．

3. 3. 1 JML が付加された Java スケルトンコードの構文定義
JML が付加された Java のスケルトンコードが記述できるモデルの構文定義を行った．Java については，クラス宣言, 修飾子, クラスのフィールド変数とメソッドの宣言を対象として構文を定義した．これは正しく変換を行うために，変数の型の情報やそれぞれの名前が必要となるためである．

JML の部分は今回は試作型として JML の Reference Manualで定義されている式の部分の構文と演算のみを扱った．JML から OCL への変換を実現する際に JML は OCL と比べて実装に近い言語なので具体性が高く, OCL では表現できないものが存在する．例として，JML では代入演算やシフト演算が存在する
が，OCL ではそれに対応する演算が存在しない．このような変換を定義できない構文や演算は，構文定義の時点で予め除いている．Xtext で生成されるエディタは構文定義に従ったエディ
タを生成することから，対応していない構文を除去しておくことで，変換可能なコードのみが入力できるようになり，ユーザは容易に対応している JML 式が理解できる．

3. 3. 2 JML から OCL への変換ルールの定義
JML から OCL への変換ルールの定義の一部を表 3 に示す．
JML から OCL への変換は，基本演算についてはほぼ 1 対
1 で OCL・JML 間の対応を取ることができ，JML の演算子をOCL の演算子へと変換するだけでよい. ただし，一部の演算子については，被演算子の順序を入れ替えるなどする必要がある
ものも存在する．
また，JML の文法は，Java の文法を踏襲している．例えば“+演算子”については，数値型 + 数値型 など型が同じもの同士の演算以外にも，文字列型 + 数値型 という形も記述可能である. しかし，OCL では異なる型同士での演算には対応していな
いため，対応することができない．また，JML では 文字列型＋文字列型 のように数値型以外も “+演算子”を使う事ができる．

しかし，OCL では文字列型と文字列型なら 文字列型.concat(文字列型) のように表現しなければならないため，型情報を考慮して変換をしなければならない.
ループ演算に関しては，OCL の exist や forall 演算は Collec-

tion 型の演算として存在しているが，JML の exist や forall は
OCL と異なり，Java における for 文のような記述を行うこともできる．そのため，JML における全てのループ演算を OCL で対応することはできない．そこで今回は，Collection に対して演算している場合のみ JML から OCL へ変換し，それ以外の場
合はエラーを出力する形で対応した.

3. 4 型 推 論
二つのオブジェクトが同値であることを評価する演算に関して，OCL では任意の型において ‘=’ が用いられるが，JML
では基本データ型の比較には ‘==’ が用いられ，参照型には

equals() メソッドが用いられる．変換を正しく実行するためには，変数の型などを正しく判別する必要がある．
ここでは，変換を行う前にまずクラス名・メソッド名・変数名などをキーとして型の情報を返す Map を作成し，構文内で変数などが現れた際に，作成した Map から型を取得することで対応している．本来はエディタ上のモデルチェックの段階で判別すべきと考えられるが，現在は変換を行うまでは型の情報についての正しい判別行うことができない状態である．

4. 評 価 実 験
この章では，評価実験について述べる．

4. 1 実 験 概 要
本研究では作成したツールを小規模なプロジェクトに対して適用した．実験 1 は実験対象プログラムに記述された JML を作成したツールで変換して, どの程度意味的に正しく変換が行えるかどうかを検証する．実験 2 では RTE 適用可能性を確かめるために作成したツールで JML から OCL へ変換した結果を，既存の変換ツールで再び JML へと変換し, どの程度元の表現を再現できるか検証する．

4. 2 計 測 内 容作成したツールで変換した結果を評価する指標として以下の—4—context ContainerItem::toString()::String
post : result.matches(’ContainerID.’[type error][type error][type error][type error])context ReceptionDesk::deliveringOrder()::List
post : requestList->forAll(r:Request|r.getAmount() > 0)
post : requestList and r=(r)@pre and ->forAll(
r:getRequestState() = StockState.SHORTAGE)

図 7 JML から OCL へ変換できなかった例 (出力結果)

演算,String 型と数値型の+演算などがあげられる．

4. 3. 2 実

験2

実験 1 において，JML から OCL への変換で意味的に正しく
図 5 在庫管理システムの UML クラス図変換できた式の数は 103 個である．それらの 103 個の式を，試作型の OCL から JML への変換ツールに入力として与えたとこ

2 点を計測する．

ろ，全て変換対象として正しく認識されることが確認された．

変換率 JML から OCL へ，意味的に正しく変換できた数．

JML から OCL への変換で正しく変換できなかったものを含め逆変換率 JML から OCL へ変換し，再び JML に変換したとると 76%となるが，正しく OCL に変換できた式に関して言えきに意味的に同じ表現に戻った数．

ば，OCL から JML への変換可能率は 100%となった．このこ

変換率については，入力として与えた JML のうち，OCL へ意とから JML から OCL への変換に関しては，問題なく変換され味的に正しく変換できた割合とする．逆変換率については，入ていることがわかる．ただし，現在ツールの変換ルールの部分

力として与えた JML と 2 段階の変換を経て再び JML に変換さが実装途中の段階であることから，OCL から JML への変換結れた結果を比較して，意味的に同じ表現に戻る割合とする．

果にバグがある部分もいくつか見つかった．結果としては 103

4. 3 実 験 結 果
4. 3. 1 実

験の入力した OCL 式のうち，87 の式は正しく変換され，変換率1

実験 1 では，図 5 で示す在庫管理システムを用いて評価をは 84.5%となり，16 の式は変換結果にバグが見つかった．図 8，
図 9 に変換できなかった場合の一部を具体例として示す．

行った．
図 5 は，我々の研究グループの過去の研究 [19] で作成したUML であり，既にすべてのメソッドに JML が記述されている．

pre : o.oclIsTypeOf(Request)
post : result = (receptionDate.getTime()(o.oclAsType(Request)).getReceptionDate())

在庫管理プログラムに記述されている事前条件, 事後条件, 不変
条件の数は全部で 130 で, それらについて変換を適用した．意.oclAsType(Integer) or result = 0
op compareTo(o : Object)

味的に正しく変換できた条件数は 102 で変換率は 78.4%となっ

図 8 OCL から JML へ変換できなかった例 (入力)た．図 6，図 7 に変換できなかった場合の一部を具体例として示す．
/*@
requires o.getClass().equals(Request);/*@
ensures \result.matches("containerID." + containerID

ensures (\result == (receiptionDate.getTime()((o.oclAsType(Request)).getReceiptionDate()))+ "CarryingDate | " + carryingDate + "\n{1}").oclAsType(Integer)) || (\result == 0);@*/
String toString(){@*/}

public void CompareTo(Object o){/*@}ensures (\forall Request r; requestList.contains(r);図 9 OCL から JML へ変換できなかった例 (出力結果)

r.getAmount() > 0);
ensures (\forall Request r; requestList.contains(r)&& r.getAmount() != \old(r.getAmount());
r.getRequestState() == StockState.SHORTAGE);@*/

oclAsType メソッドは構文定義には記述されていたが，変換ルールには実装されていないという実装漏れが見つかった．う
まく変換されなかった 16 の式は全て修正方法は考察できてい

List deliveringOrder(){}

図 6 JML から OCL へ変換できなかった例 (入力)

正しく変換できなかった場合は forall などのループ演算で変数が複数宣言されていたり条件が複雑な場合,\type 演算,\typeof

るので，今後修正していきたいと考えている．

4. 4 考察

実験 1 については，実験結果の変換率を見てみると変換率は 78.4%となっている．今回は試作型として主に基本演算の変換を実現したので全てを変換することはできなかった．しかし

78.4%という変換率は JML 記述の多くを基本演算が占めている—5—

ことを表していて, 変換の有効性を確かめることができた．

び JML から OCL への変換ツールを用いて行うことを考えて変換できなかったものの一部についての考察を行なっていく．

いる．

まず JML の \type と \typeof といった引数として与えた変数の謝辞

本研究の一部は科学研究費補助金基盤 C（21500036）

型名やリストなどの要素の型名を返す演算については変換出来と文部科学省「次世代 IT 基盤構築のための研究開発」（研究開なかった．これは OCL では型名を求める演算は存在していな

発領域名：ソフトウェア構築状況の可視化技術の普及）の助成

いためである．この変換に関しては，JML の解析の時点で引数による．また，Xtext について教えていただいた公立はこだての型の情報を求めておき，OCL には直に型名を出力するという未来大学の田中明氏に感謝する．

対応が考えられる．
実験 2 については，実験結果の逆変換率は JML から OCL で意味的に正しく変換できたものについては 84.4%となった．変
換結果には正しくない表現になっているものが存在したが，これは逆変換に使用したツールが試作段階で，デバッグが完了していなかったり実装の漏れが存在するためである. 入力として与えた OCL は変換可能と認識されたので品質に問題はないが，変換部分が不完全なのでこのような結果になったと考えられる．
これらより JML から OCL への変換は実際に他のツールなどに適用できる形に変換できていて，生成された OCL の品質に問題がないことが確認できた. 変換できなかったものについて
は，変換は 1 対１で対応しているので実装するときのミスであり，今後追加実装を行うことで正しい変換を実現できると考えている．

5. あ と が き
本稿では仕様記述レベルでの RTE による開発を支援すること，様々な制約記述言語間での相互変換の 2 点を目標とした，

OCL から JML への変換及び，その逆変換である JML から OCLへの変換についての具体的な実装方法，及び試作型として実装したツールについての簡単な評価を行った．
今後の課題としては，まずツールを完成させることである．
現在はまだ試作段階であり，対応し切れていない部分も存在しているので，それらの点を実装に移していく．例えば OCL から JML に関して言えば，Undefined の扱いなどが現状不十分であるので，今後正確に対応していくことなども課題として考えている．
ツールの実装が完成後には，追加実験を行うことを考えている．ツールの評価に関しては，まず OCL から JML への変換とJML から OCL への変換のそれぞれについて評価を更に詳細に行おうと考えている．

OCL から JML への変換ツールに関しては，現在は変換成功数などについての簡単な評価のみ行った状態である．今後は

esc/java2 や jml4c などの JML 用の検査ツールに対して生成された JML を適用した場合の結果と，人手によって記述された

JML を適用した場合の結果を比較・検証することを考えている．
JML から OCL への変換ツールに関しては，Octopus のような OCL 式検証ツールを利用して，生成された OCL を検証，人手によって記述された OCL 式と比較したコードの可読性の評
価などを考えている．
また，OCL-JML 間の相互変換をツールを利用して繰り返し文

献[1] A.G. Kleppe, J. Warmer, and W. Bast, MDA explained: the model
driven architecture: practice and promise, Addison-Wesley Longman
Publishing Co., Inc. Boston, MA, USA, 2003.
[2] G. Engels, R. Hücking, S. Sauer, and A. Wagner, “Uml collaboration
diagrams and their transformation to java,” UML1999 -Beyond theStandard, Second International Conference, pp.473–488, 1999.
[3] 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.
[4] Object Management Group, “Ocl 2.0 specification,” 2006.
http://www.omg.org/cgi-bin/apps/doc?formal/06-05-01.pdf.
[5] G. Leavens, A. Baker, and C. Ruby, “Jml: A notation for detailed design,” Behavioral Specifications of Businesses and Systems, pp.175–
188, 1999.
[6] B. Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle
River, NJ, 1992.
[7] 尾鷲方志，岡野浩三，楠本真二，“メソッドの自動生成を用いた
ocl の jml への変換ツールの設計,” ソフトウェア工学の基礎 XVI,
日本ソフトウェア科学会 (FOSE 2009)，pp.191–198，近代科学社，
2009．
[8] 宮澤清介，花田健太郎，岡野浩三，楠本真二，“Ocl から jml への変換ツールにおける対応クラスの拡張と教務システムに対する適用実験,” 信学技報，vol.110，no.458，pp.115–120，2011．
[9] Eclipse Foundation, “Xtext - Language Development Framework”.
http://www.eclipse.org/Xtext/.
[10] N. Medvidovic, A. Egyed, and D.S. Rosenblum, “Round-trip software engineering using uml: From architecture to design and back,”
1999.
[11] S. Sendall and J. Kuster, “Taming model round-trip engineering,” In
Proceedings of Workshop Best Practices for Model-Driven Software
Development, pp.1–13, 2004.
[12] Y. Cheon and G.1 Leavens, “A simple and practical approach to unit
testing: The jml and junit way,” ECOOP 2002 Object-Oriented Programming, pp.1789–1901, 2006.
[13] Object Management Group, “Documents associated with meta
object facility (mof) 2.0 query/view/transformation, v1.1,” 2011.
http://www.omg.org/spec/QVT/1.1/PDF/.
[14] F. Jouault, F. Allilaire, J. Bézivin, and I. Kurtev, “ATL: A modeltransformation tool,” Science of Computer Programming, vol.72,
no.1-2, pp.31–39, 2008.
[15] “Uml2java”. ”http://uml2java.sourceforge.net/”.
[16] A. Hamie, “Translating the object constraint language into the javamodelling language,” In Proc. of the 2004 ACM symposium on Applied computing, pp.1531–1535, 2004.
[17] M. Rodion and R. Alessandra, “Implementing an ocl to jml translation tool,” 信学技報, vol.106, no.426, pp.13–17, 2006.
[18] 林千博，名倉正剛，高田眞吾，“ajax アプリケーションを対象としたラウンドトリップエンジニアリング支援手法，” ソフトウェア工学の基礎 XVI, 日本ソフトウェア科学会 (FOSE2011)，pp.51–60，
近代科学社，2011．
[19] 尾鷲方志，岡野浩三，楠本真二，“JML を用いた在庫管理プログ
ラムの設計と ESC/Java2 を用いた検証，” 電子情報通信学会技術報告，vol.107，no.176，pp.37–42，2007．

適用し続けることができるか，相互変換を繰り返しても意味的に正しさを保てるか，などの評価を作成した OCL から JML 及—6—