アスペクトを用いた表明の記述
石尾隆 ††

神谷年洋 ‡

楠本真二 †‡

大阪大学 大学院情報科学研究科〒 560-8531 大阪府豊中市待兼山町 1-3

井上克郎 †

独立行政法人 科学技術振興機構 さきがけ
〒 560-8531 大阪府豊中市待兼山町 1-3

契約による設計や Java や C++ などの assert 文といった機構は，一般に表明と呼ばれる．しかし，オブジェクト指向プログラミングにおいては，表明は再利用を阻害してしまう場合があり，また複数のオブジェクト間の関係に対して表明を記述することができないなど，いくつかの制約がある．アスペクト指向プロ
グラミングは，オブジェクトを横断した要素を単一のモジュールとして記述することができるため，アスペクトとして表明を記述することで表明の持つ弱点を補うことができると考えられる．本稿では，Java を題材に，アスペクトとして表明を記述することで得られる利点について議論する．

Assertion with Aspect
Takashi Ishio† Toshihiro Kamiya‡
Shinji Kusumoto† Katsuro Inoue††Graduate School of Information Science andTechnology, Osaka University
1-3 Machikaneyama-cho, Toyonaka,‡PRESTO, Japan Science and Technology Agency
1-3 Machikaneyama-cho, Toyonaka,
Osaka 560-8531, Japan

Osaka 560-8531, Japan

Programmers use assertion to enforce design by contract. However, in Object-Oriented Programming,assertion has few drawbacks. One drawback is that assertion may prevent the reuse of a class. Anotheris that programmers cannot express assertion about inter-object relations. Using Aspect-Oriented
Programming technique, which enables to describe a crosscutting concern in one module, programmerscan write assertions of inter-object relations. In this paper, we discuss the eﬀect of writing assertions
as aspects.

-1-

1

はじめにアスペクトとして分離するプログラミング技術を利用して，複数のオブジェクトを横断した条件や契約による設計（Design by Contract ）は，部

オブジェクト間の相互作用にかかわる条件を分離

品ごとの責任の範囲を明確に表現することで，ソ記述する方法を提案する．

フトウェアを機能部品に分解する際の安全性を向オブジェクトから一部の条件をアスペクト側に上する．契約による設計は，手続きのような処理分離する利点は， 特定の環境に依存した表明など単位において，その開始時に成立しているべき条をオブジェクトから分離して記述することが可能

件（事前条件）と，終了時に成立しているべき条件になることと，必要に応じて表明の追加および取（事後条件）とを記述することで実現される．契約り外しができるようになることである．

による設計や，Java や C++ における assert 文とまた，提案手法では，制御フローに関する条件式

いった機構は，一般に表明 (assertion) と呼ばれる．

を導入する．これは，AspectJ で導入された cﬂow

事前条件は手続きへの誤った入力を防ぎ，事後pointcut の概念を表明に特化したものである．特条件は手続きの誤った出力を防ぐ役割を持つ [16]．

定の呼び出し側に限定した条件を記述することで，事前条件が満たせない場合は手続きを利用する側，開発者の意図をより明確に表現できる．

事後条件が満たせない場合は手続きを実装する側

以降，2. では背景の詳細について，3. では提案の責任となる．このような責任の分離は，開発者手法について説明する．4. では例題に対してどのが作業の分担を明確にできるほか，欠陥の原因をように働くかを評価を行い，5. で関連研究につい切り分ける際の指標となるといった効果がある．て述べる．最後に 6. でまとめる．

オブジェクト指向プログラミング言語では，しばしばクラスが部品の単位となり，クラスの持つ2

背景

メソッドごとに事前条件，事後条件を記述する．契2.1

契約による設計

約による設計を言語要素として取り込んだものと契約による設計（Design by Contract ）は，部しては Eiﬀel[14] などがある．Eiﬀel では，クラス品ごとの責任の範囲を明確に表現することで，ソのメソッド単位での事前条件および事後条件を，メフトウェアを機能部品に分解する際の安全性を向

ソッド本体とは区別して記述することが可能であ上する．契約による設計は，手続きのような処理る．また，例外 (Exception) を，事前条件が満たさ単位において，その開始時に成立しているべき条れているにもかかわらず事後条件が満たせない状件（事前条件）と，終了時に成立しているべき条況と規定している．Java や C++ で同様の記述を件（事後条件）とを記述することで実現される．

可能にするツールとして，Larch[8]，iContract[9]，事前条件はコンポーネント側の要求をアプリケー

jContractor[11]，JML[10] などがある．

ションに伝えることで手続きへの誤った入力を防しかし，メソッド単位で条件を記述する場合，メぎ，事後条件は，コンポーネントの誤った処理からソッドの呼び出し側に対する条件や，複数のオブアプリケーションを保護する役割を持つ [16]．オ

ジェクトが連動する一連の処理に対する条件など

ブジェクト指向プログラミング言語の場合，事前はうまく記述することができない，この原因は，次条件と事後条件はオブジェクトのメソッド単位でのように考えられる．

記述される．事前条件が満たせない場合は手続き(1) オブジェクトが他のオブジェクトに依存した条件を持っている，を利用する側，事後条件が満たせない場合は手続(2) 制御フロー（呼び出し側オブジェクト）に関する情報を使えない，分離は，開発者ごとの作業の分担を明確にし，欠きを実装する側の責任となる．このような責任の陥の原因を切り分ける際の指標となる．

(3) 一時的に条件を崩している処理中のオブジェク
トが，再帰的に呼び出されることがある．

その途中の動作が正しいことを確認するために，本稿では，アスペクト指向プログラミングと呼プログラム文として表明を記述することができる．

ばれる，複数のオブジェクトを横断した関心事を言語処理系によって多少異なる場合もあるが，表開発者は，手続きの開始と終了の時点以外にも，-2-

(1) 過度の表明が，再利用の柔軟性を低下させるこ

明文 assert(expr) は，次のような意味を持つ．とがある．

expr = true →expr = false →

何もしない
例外を送出する(2) メソッド呼び出し側に対する仮定が記述できない．

(3) 複数オブジェクトの一連の動作に対する条件が表明には，開発者のためのドキュメントとして記述できない．の役割もある．開発者は，ソフトウェア部品の個々これらの問題をもたらした原因としては，表明の事前条件，事後条件，手続き途中に配置されたによって言及可能なのは，それが帰属するオブジェ

表明文を見ることで，その部品を使うために必要クトおよびそのオブジェクトからアクセス可能なな条件，機能の特性，変更する際の注意点などを知範囲に限られることが挙げられる．これらの問題ることができる．ソフトウェア部品の使用者がそは，具体的には以下のような制約として表れる．の部品の実装詳細へ過度に依存することはソフト(1) 再利用の柔軟性: 表明は，他のオブジェクトにウェアの変更容易性を損なう原因となるが，それを依存した条件を持っている場合がある．

防ぐために表明は有効である [13]．また，eXtreme

Programming[3] をはじめとするアジャイル型の開(2) 呼び出し側に対する仮定: 制御フロー（呼び出発プロセスでは，表明を用いてプログラムの動作し側オブジェクト）に関する情報を表明としてが正しいことをテストするといった形で表明を活扱えない．

(3) オブジェクトを横断した表明の条件: 複数のオブジェクトから構成された条件は，オブジェク用している．
契約による設計を言語要素として積極的に取りトに帰属させることが困難な場合がある．

込んだものとしては Eiﬀel[14] がある．オブジェク
ト指向プログラミング言語である Eiﬀel では，ク以降，再利用の柔軟性については 2.3 で，呼びラスのメソッド単位での事前条件および事後条件

出し側に対する仮定は 2.4 で，複数のオブジェクを，メソッド本体とは区別して記述することが可

トを横断した条件については 2.5 で述べる．

能である．また，各メソッドに共通な事前条件，事2.3

後条件をクラス不変条件として独立させて記述で再利用の柔軟性

表明はソフトウェア部品の品質や理解容易性にきるほか，例外 (Exception) を，「事前条件が満た寄与する一方で，プロジェクトごとの要因によっされているにもかかわらず事後条件が満たせないて一部の表明が冗長になる場合や，過度に課せら状況」と規定している．

れた条件が再利用を阻害する場合がある．ソフト

C++ や Java のように言語要素として契約によ

ウェア部品についての表明は，次の二つに分類さる設計を取り入れていないプログラミング言語でれる．

も，プログラム文として表明を記述するための表• アプリケーション（利用者）依存の条件．すな
わち，ソフトウェア部品が提供している機能の明文が用意されている．また，これらのプログラ
ミング言語において，事前条件，事後条件の記述うち，アプリケーションが必要とする機能だけを可能にするツールとして Larch[8]，iContract[9],を提供するための条件．

jContractor[11], JML[10] など，様々なツールが研究，開発されている．その一方で，設計段階で契約• ソフトウェア部品（提供者）依存の条件．すな
わち，ソフトウェア部品が機能を提供するためによる設計を利用するため， UML 上でオブジェに使用しているアルゴリズムの制約などから生クトの制約を記述するための言語 OCL なども提じる条件．

案 されている [18]．

2.2たとえば，任意のクラスのオブジェクトを格納

表明の制約表明（事前条件，事後条件を含む）の記述はオできるような List クラスの利用者が，実際にはString クラスのオブジェクトだけを格納したいとブジェクトの再利用の安全性を高めるが，それという要求を持っている場合がある．このとき，任意同時に，次のような問題がある．のオブジェクトを格納できるというのは List の持-3-つ条件であり，String だけを格納するというのはstrongアプリケーションの持つ条件である．ここで，Listを作成した開発者が，設計や実装において使用すInappropriate
ExtensionSpecialization

Original
Component

requireる型を限定したり，表明によって String だけを格納することを選ぶと，アプリケーションの安全性はweak向上する．しかし，将来の再利用において，String以外のクラスに List を適用しようとするときにはweak障害となる．このような，アプリケーション側のBehavioral
Subtyping

Generalization

ensurestrong

図 1: 表明による拡張の制約

制約については，クラス本来の制約とは分離しておくことが望ましい．

明を目的に応じて分類して記述するといった管理クラスの再利用は，しばしば継承という形で行わも可能となる．詳細については，3. で述べる．

れる．このとき，導出されたクラスのオブジェクト

2.4は，基本クラスのオブジェクトの代替として振舞う呼び出し側に対する仮定の記述ことが求められる．この条件のことを，Behavioral

開発者は，作成するメソッドが特定のオブジェSubtyping と呼ぶ．Behavioral Subtyping を満たクトに利用されることを想定して実装を行っていすためには，導出されたクラスは，基本クラスの事る場合がある．このとき，呼び出しを行うオブジェ

前条件が満たされた状態ならば必ず動作し，かつクトに対する暗黙の情報が，インタフェースに埋基本クラスが保証している事後条件は少なくともめ込まれている場合がある．たとえば，平方根を整満たさなければならない [5]．この関係を，図 1 に数に対して求める関数を作成する際，呼び出し側示すように事前条件 (require) と事後条件 (ensure)の関数が必ず自然数しか扱っていないと決まっての２つの軸で見ると，事前条件を弱めること，事いるのであれば，開発者は，入力値を調べるコー

後条件を強めることは許されるが，特定の環境にドを記述するとは限らない．

特化する，つまり事前条件を厳しくするような実また，複数のオブジェクトが連携するとき，ある装は許されない．たとえば，あるクラスを基に，特特定のオブジェクトからの呼び出しにのみ処理を定の環境に限定して特化したい場合，リファクタ許したい場合がある．たとえば，デザインパターリング手法「インタフェースの導出」と「メソッドンのひとつである facade パターン [7] は，あるサの引き上げ」[6] を適用することで，基となったクブシステムを構成するオブジェクト群へのアクセラスと新しく作成するクラスの共通部分のインタスを集中管理する単一の facade オブジェクトを導フェースを新しく構築し，Behavioral Subtyping入する．これによって，オブジェクト群の取り扱を維持する必要がある．しかし，基本となるクラス

いを簡単なインタフェースだけを通じて操作するが書き換え可能でない場合には対応できず，また，ことができる．このような場合，facade 経由での書き換え可能である場合でも，元のインタフェースみアクセスを許可し，それ以外のアクセスを禁止を使用していた部分を書き換える必要があり，かするような表明が考えられる．このようなアクセなりの手間となってしまう [17]．このような場合，

ス制限は，Delegation Layer[15] のようなラッパー

既存の表明が必要に応じて解除できることが重要オブジェクトを利用する場合にも生じる．
その他にも，呼び出し側の状態に依存した条件となる．
これらの問題に対処するため，本稿ではアスペといった記述は，現状の表明記述言語では記述すクトを用いた表明の記述を提案する．表明は，検査ることができない．これは，従来，表明がコンポーが成功している限り対象プログラムの振る舞いにネント（呼び出される側）のみに依存し，呼び出は影響を与えないことから，開発しているソフトし側に対する条件を書けないためと考えられる．

ウェア部品から容易に切り離せるようにアスペク

本稿では，この問題を解決するために，制御フトして実装することが適当である．表明をアスペローに関する表明の記述を導入する．詳細についクトとして本来のクラスから分離することで，表ては，3. で述べる．

-4-

2.5

オブジェクトを横断した表明の条件

メソッドを作成し，そのメソッドにアスペクトを関連付けることで，このような実行時点に適用可

複数のオブジェクトから構成された条件は，単能な表明文を実現する．

一のオブジェクトに帰属させるのは困難な場合が本稿では，プログラミング言語要素としての型ある．
例として，Model と View のオブジェクト間のチェックなどの議論については省略し，どのよう相互参照が１対１に対応している，という条件をな記述を目標としているかの基本的なアイディア考える．このとき，新しい View に変更するといっについて説明する．

た更新作業を行うと，その作業途中で一時的に表まず，クラス側の記述は，従来と同様である．表

明が崩れる場合がある．このような処理の途中で明専用の関数を呼び出すような記述を，表明文とは，現在が更新作業の途中であるから相互参照にして記述する．

関する表明の検査はしない，という情報をどこか// f is a valid file stream.
assert(FileIsOpened(f));に記憶しておく必要がある．しかし，どのインスタンスが更新中であるかという情報を Model 側とView 側に分散させると，一貫性のある状態の保持上の文で FileIsOpened(f) として呼んでいる真が難しくなる．

偽判定の実装を，アスペクト側で行う．

このようなオブジェクト間の関連に対する表明や，その実現に必要なフラグなどをアスペクトに

aspect FileAssertion {分離しておくことで，関連しあったオブジェクト

ASSERT FileIsOpened(FileInputStream f){ return f.ready(); }単体での再利用性や，変更容易性を向上できると考えられる．

3}

横断的な表明の記述
本章では，表明をどのようにアスペクトに分離

便宜上，ASSERT という修飾子を記述している

するか，また制御フローをどのように表明としてが，本体は，真偽値を返すメソッドとして実装される．ASSERT と通常のメソッドとの違いは，戻り記述するか，という方法について議論する．

値が真偽値に限定されていることと，本体の定義

表明文は，クラスの開発者が，プログラム文とが複数あるかもしれないこと，である．

してメソッド中の任意の位置に記述する．Java で実行時には，クラス開発者が準備した assert とあれば assert キーワードが，他の言語でも類似いう実行時点で連動するアスペクトが条件の評価の言語要素あるいは関数などによって実現されてを行い，すべての条件が通過したかどうかをテスいる．

トする．

事前条件および事後条件は一般に，メソッド実

この方法の有利な点は，アスペクト実装者など，行の前後に検査される表明文をアスペクトを用い他のクラス開発者が，後から表明を追加できるこて記述することで実現可能である．従って，以降，とである．

表明はすべて表明文によって記述するものとし，表3.1

明文の記述法のみについて議論する．参考までに，制御フローに関する表明事前条件を AspectJ で記述した例を図 3 に示す．

メソッドの再帰呼び出し時は，一部の不変条件

表明文は，アルゴリズムの正しさなどを特定のが崩れている可能性がある．たとえば，不変条件実行時点で検査するために記述するが，AspectJが崩れた状態から復帰する作業に必要なメソッドで採用されているようなメソッド呼び出しなどを呼び出しなどが該当する．

単位とした Join Point 記述ではループの先頭や条制御フローに対応した表明記述を可能にするこ

件文の終了時といった実行時点に適用しにくい．そとで，そのような条件に対処する．そのために，

こで，表明文そのものは，従来と同様の形式で記AspectJ の pointcut 指定子である cﬂow を論理式として使用する．

述を行うが，表明文に用いる真偽値を返すような-5-

// Precondition: f is a valid input stream.
before(FileInputStream f) : this(f) && execution(* MyFileReader.read(..)) {assert(f.ready());}
図 2: assert 文と AspectJ を用いた事前条件の記述例
Sheet

has-aの値を評価する必要があるため，再帰的に処理がCell進行する．セル間に循環参照があった場合，値決

is-a

Empty

Value

Expression

定の処理が無限ループに陥る．循環参照に陥ってStringCellいないかどうか，表明を用いて検査を行う．

is-aSumMax

図 4 に，循環参照となるような呼び出しはエラー

Countとするような表明を，値評価メソッド value() の

図 3: 表計算プログラムのクラス構成中に直接記述したものを示す．
この表明文を，AspectJ を用いて記述しようと

assert ( cflow (aClass.aMethod) );assert ( cflow (obj.aMethod) );すると，図 5 のように新たな例外クラスや，フラグを制御するコードを記述しなければならないこ

この表明文は，引数として指定されたシグネチャ
aClass.aMethod が呼び出しスタック上に積まれてとがわかる．従来の Java のみで実現しようとすいるかどうかを真偽値として返す．obj.aMethod とた各クラスに分散することになる．

記述した表明は，クラスの部分を特定のオブジェ

5

関連研究

5.1

アスペクト指向プログラミング

ると，AspectJ で作成した記述が，実際に関連しクトのみに限定した場合である．これによって，特定のオブジェクト，メソッドから呼ばれているか否かを判定することができる．基本的には，事前アスペクト指向プログラミングは，横断的関心条件として記述することで，特定の制御フローの事の分離を基本的な考え方としている．複数のオ下でのみ条件を検査する，といった用法を想定しブジェクトを横断した表明をアスペクトとして記ている．

述することが自然であると考えられる．AspectJ4を用いると，容易に事前条件と事後条件を記述す例題と評価ることができる．しかし，プログラム文の特定の例題として，簡単な表計算アプリケーションを位置で表明を検査するという場合には，一般的な用いる．主要な構成要素は Sheet，Cell という２Join Point として記述することは難しい．本稿で種類のクラスである．Sheet は表であり，Cell がそ提案した手法を用いれば，表明を検査するメソッの構成要素である．Cell 自体は抽象クラスであり，ドの本体を，アスペクト側から改変することで，ク

Empty（空），Value（整数値），StringCell（文字列），Expression（式）のいずれかを格納する．

ラス側に記述した表明は簡潔に済ませながら，アスペクト側にコンテキストに応じた表明を分離しExpression は，ある一定範囲の有効な（Empty でない）Cell の個数を数える Count と，ある一定範て記述することができる．

5.2

囲の Value の値の和を計算する Sum，最大値を求Java Modeling Language (JML)

める Max がある．クラスの構成を図 3 に示す．

Java Modeling Language (JML) [10] は，Javaカンマ区切りで記述されたテキスト形式のファクラスの振る舞い仕様を記述するための言語であイルから表の各セルの状態を読み込み，式の値をる．JML の記述は Java ソースコードのコメント計算し，結果を出力する処理を考える．このとき，
Sum オブジェクトは，他のセルの値を調べにいくに埋め込まれる．JML では，オブジェクトの状態ことになる．調べるセルが他の Sum オブジェク

件を記述することができる．その他にも，事後条

トや Max オブジェクトであれば，先にそのセル件を満たせない例外発生時の状態についても記述を表現するモデル変数を使って事前条件，事後条-6-

class Cell {public abstract int value();:}class Expression extends Cell {:}class Sum extends Expression {// return Iterator for SUM target cells.
Iterator getRangeIterator() {:}// return the sum of cells’ value.
public int value() {assert(!cflow(int this.value())); // prohibit recursive callint sum = 0;
for (Iterator it=getRangeIterator(); it.hasNext(); ) {sum += ((Cell)it.next()).value();}return sum;}:}

図 4: 循環参照を防ぐ表明を提案手法で記述した例
class AssertionViolation extends RuntimeException {}pointcut execValue(Expression e): this(e) &&execution(int Expression.value());
boolean Expression.now_executing = false;
Object around(Expression e): execValue(e) {if (e.now_executing) throw
new AssertionViolation("Cyclic Reference is Detected !");
e.now_executing = true;
Object o = proceed(c);e.now_executing = false;
return o;}

図 5: 循環参照を防ぐ表明を AspectJ で記述した例
することができ，柔軟性の高い記述が可能であるとでプリプロセッサを簡単に開発プロセスに組み[4]．しかし，複数のオブジェクトが連動した場合込めるようにすることを考えている．に，「誰の」不変条件であるかが明確でない場合にど課題としては，表明を定義している真偽値を返のように記述するか，ガイドラインが存在しない．

すメソッドは副作用を持つべきではないが，それJML を AspectJ 向けに拡張することも提案されている [19] が，AspectJ によって導入された cﬂowを強制する手段がないという問題がある．C++ でなどのいくつかの要素をサポートしていない．そことを開発者が言明する形式を用いることで，表のため，今回提案したようなオブジェクト間の関連明として使用されているメソッドが副作用を持たについての表明を記述することには不向きである．

ないと宣言されていない場合に警告を出すといっ

6

た方法によって，問題を緩和することが可能であ用いる const キーワードのような，副作用がないまとめと今後の課題ると考えられる．

オブジェクトを横断した表明に対して，現在利参考文献

用可能な記述法では，直接的な記述をすることはできない．解決策として，アスペクトを用いた表明[1] The Apache Ant Project.の付加と，制御フローを用いた表明の記述方法を

http://ant.apache.org/提案した．提案した言語要素については，AspectJ[2] The AspectJ Team: The AspectJ Programming Guide.に変換するプリプロセッサとして実現する予定である．ビルドツールである Ant [1] と連携するこ-7-http://dev.eclipse.org/viewcvs/indextech.cgi[12] Kiczales, G., Lamping, J., Mendhekar,/˜checkout˜/aspectj-home/doc/progguide/A., Maeda, C., Lopes, C.V., Loingtier, J.
and Irwin, J.: Aspect Oriented Program-[3] Beck, K.: Extreme Programming Explained.

ming. In Proc. of the 11th annual European
Conference for Object-Oriented Programming

Addison-Wesley Pub Co., Boston, MA, 1999.

(ECOOP97), vol.1241 of LNCS, pp.220-242,[4] Burdy, L., Cheon, Y., Cok, D., Ernst, M.,

1997.

Kiniry, J., Leavens, G. T., Rustan, K., Leino,M. and Poll, E.: An overview of JML tools
and applications. In Proc. of 8th Interna-[13] McCamant, S. and Ernst, M. D.: Predicting

tional Workshop on Formal Methods for Industrial Critical Systems (FMICS ’03), pp.

In Proc. of the 11th Foundations of Software
Engineering (FSE 2003), pp.287-296, 2003.

73-89, Vol. 80 of Electronic Notes in Theoretical Computer Science, 2003.

[14] Meyer, B.: Object Oriented Software Con-

Problems Caused by Component Upgrades,struction. Prentice Hall, New York, NY, 1988.
[5] Findler, R. B., Latendresse, M. and Felleisen,
M.: Behavioral Contracts and Behavioral
Subtyping. In Proc. of the 9th Foundationsof Software Engineering (FSE2001), 2001.
[6] Fowler, M., Beck, K., Brant, J., Opdyke, W.
and Roberts, D.: Refactoring: Improving theDesign of Existing Code. Addison-Wesley PubCo., Boston, MA, 1999.

[15] Ostermann, K.:
Dynamically Composable Collaborations with Delegation Layers.
In Proc. of the 16th European Conference
on Object-Oriented Programming (ECOOP2002), pp.89-110, 2002.
[16] Romanovsky, A.: Exception Handling in
Component-based System Development. In
Proc. of the 25th Annual International Computer Software and Application Conference[7] Gamma, E., Helm, R., Johnson, R. and Vlissides, J.: Design Patterns. Addison-Wesley
Pub Co., Boston, MA, 1995.
[8] Guttag, J. V., Horning, J. J. and Wing, J. M.:
The Larch Family of Speciﬁcation Languages.

(COMPSAC 2001), pp. 580-586, 2001[17] Tip, F., Kiezun, A. and Baumer, D.: Refactoring for Generalization using Type Constraints. In Proc. of 18th Annual Conference on Object-Oriented Programming, Sys-IEEE Software, 2(5), p.24-36, Sept.1985.

tems, Languages, and Applications (OOPSLA 2003), pp.13-26, 2003.

[9] iContract HomePage. http://www.reliablesystems.com/tools/iContract/iContract.htm[10] JML

Reference,[18] Warmer, J. and Kleppe, A.: The Object
Constraint Language: Precise Modeling withUML. Addison-Wesley Pub Co., Boston, MA,

http://www.dc.ﬁ.udc.es/ai/tp/jml/JML/docs/jmlrefman/jmlrefman/

1998.
[11] Karaorman, M., Holze, U. and Bruno,
J.: jContractor: A Reﬂective Java Library to Support Design By Contract,[19] Zhao, J. and Rinard, M.: Pipa: A Behavioral Interface Speciﬁcation Language for AspectJ. In Proc. of Fundamental Approaches toSoftware Engineering (FASE) 2003, pp.150-

Technical Report, Univ. California, Santa
Barbara, Department of Computer Science

165, 2003.

(http://www.cs.ucsb.edu/labs/oocsb/papers.html).
-8-」