契約による検証

契約に基づいたアスペクト指向
リファクタリングの検証
九州工業大学大学院
情報工学研究科
朴金姫，篠塚卓，鵜林尚靖
1
発表の流れ

背景
– アスペクト指向プログラミング（AOP）
– AOリファクタリング




契約による検証
評価
関連研究
まとめ
2
背景
– アスペクト指向プログラミング（AOP）
– AOリファクタリング
3
AOP
アスペクト指向プログラミング（AOP）

AOPは横断的関心事を分離し，アスペクトとしてモ
ジュール化する技術である
– 横断的関心事：様々なクラスに散在している関心事
– アスペクト：横断的関心事をモジュール化する単位

ウィーバーによってシステム本来の機能に織り込まれる
アプリケーション機能実装
アプリケーション機能
ウィーバー
アスペクト

アスペクト
アプリケーション機能
アスペクト
AspectJ：代表的なAOP言語
4
AOP
横断的関心事
•ログ処理の例
– 赤い線はログ処理を行うコード
– 複数の場所に分散している
AspectJ. http://eclipse.org/aspectj/
5
AOP
横断的関心事
実際の振る舞い
クラス
・・・・・・
・・・・・・
アスペクト
methoda
Advice1
methoda
method1
methodb
methodc
織り込み
method1
method2
Advice2
methodb
method2
・・・・・・
methodc
method1
・・・・・・
6
AOP
AspectJ

アスペクト：
AspectJ中のモジュール単位の一つ

ジョインポイント :
プログラムが実行する時に割り込ませるコードの位
置
– メソッドの呼び出し先

ポイントカット :
織り込み先のジョインポイントを選択する記述
– プリミティブポイントカット：call , execution etc.
– ポイントカット中のジョインポイントは &&, ||, ! などの論理記号で組み合わせる

アドバイス :
指定するポイントカットによって選択されるジョイン
ポイントに差しかかったときに実行されるコード
– 実行するタイミングによってbefore，after, around などがある

ウィーバー :
クラスとアスペクトを織り合わせる処理系
7
AOP
AspectJの例
class Queue {
void enqueue (Object element) {…}
Object dequeue () {…}
boolean empty () {…}
int size () {…}
．．．．．．
void display () {
Iterator i = elements.iterator ();
．．．．．．
}
}
aspect Debugging{
．．．．．．
pointcut queueModified(Queue q):
(execution(void Queue.enqueue(Object))||execution(Object Queue.dequeue()))
&& target(q);
after (Queue q) : queueModified(q){ q.display(); }
}
8
AOリファクタリング
リファクタリング

リファクタリング
– プログラムの外部的振る舞いを変えず，内部構造を
改善する手法である
– リファクタリングを行った後，プログラムコードの理解
や修正が簡単になる

AOリファクタリング
– アスペクト指向におけるリファクタリング
9
AOリファクタリング
AOリファクタリングカタログ

Catalog of Aspect-Oriented Refactorings
--Monteiro, M. P.
①横断的関心事を抽出するためのリファクタリング
②アスペクト内部を再構造化するためのリファクタリング
③一般化を行うためのリファクタリング
10
AOリファクタリング
例に関するリファクタリングパターン
リファクタリングパターン名：
– Move Method from Class to Inter-type
典型的な状況：
– あるメソッドが含まれている関心事はクラスの関
心事ではない
推奨動作
– そのメソッドをアスペクトへインタータイプとして移
動する
11
AOリファクタリング
例におけるリファクタリング
• Move Method from Class to Inter-type
class Queue {
void enqueue (Object element) {…}
Object dequeue () {…}
boolean empty () {…}
int size () {…}
．．．．．．
void display () {
Iterator i = elements.iterator ();
．．．．．．
}
class Queue {
void enqueue (Object element) {…}
Object dequeue () {…}
boolean empty () {…}
int size () {…}
．．．．．．
}
aspect Debugging{
Queue.display (){
．．．．．．
}
}
aspect Debugging{
．．．．．．
}
12
AOリファクタリング
リファクタリングで発生する問題
• Move Method from Class to Inter-type
class Queue {
void enqueue (Object element) {…}
Object dequeue () {…}
boolean empty () {…}
int size () {…}
．．．．．．
void display () {
Iterator i = elements.iterator ();
．．．．．．
}
}
aspect Debugging{
．．．．．．
}
class Queue {
void enqueue (Object element) {…}
Object dequeue () {…}
boolean empty () {…}
int size () {…}
．．．．．．
void display () {
Iterator i = elements.iterator ();
．．．．．．
}
}
aspect Debugging{
void display () {
Iterator i = elements.iterator ();
．．．．．．
}
13
．．．．．．
}
AOリファクタリング
解決方法
リファクタリングを行った後プログラムの構造は変
わるが振る舞いが変わってはいけない
リファクタリングを行う最中に発生する問題は発見しにくい
リファクタリングの正しさを検証する
①振る舞いが正しく保存される
②構造が正しく変換される
契約：静的な構造に関する性質を表現する
14
契約による検証
15
契約による検証
契約

リファクタリングを行う前後で満たされるべきプログラ
ムの構造的性質を事前条件，事後条件として与える．
これらの条件をまとめて，契約と呼ぶ．
– 事前条件：リファクタリングを行う前，プログラムの性質
– 事後条件：リファクタリングを行った後，プログラムの性質

COW（COntract Writing language）言語で記述する
– プログラムの静的な構造や振る舞いを一階述語論理で記述
する
16
契約による検証
COWの基本述語①

構造的特徴を表す述語
class(c)
クラス
body(a, b)
アクチュエータのボディトークン列
interface(i)
i はインターフェース
abstract(x)
修飾子 abstract によって修飾される
extends(x, y)
継承関係を表す
owner(x, t)
所有関係
implements(x, y)
実装関係を表す
aspect(a)
アスペクト
constructor(a)
コンストラクタ
pointcut(p)
ポイントカット
method(a)
メソッド
beforeAdvice(a)
before アドバイス
field(v)
フィールド
afterAdvice(a)
after アドバイス
enumerator(v)
列挙子
aroundAdvice(a)
around アドバイス
parameter(v)
フォーマルパラメータ
intertypeOwner(x, c)
織り込みによる所有関係
variable(v)
アクチュエータの局所変数
target(a)
制約条件の適用先アクチュエータ
name(x, n)
名前を表現する
source(a)
織り込まれるアドバイス
17
契約による検証
COWの基本述語②

動的特徴を表す述語
entry(a, s)
a の実行開始位置はステートメント s
call(s, a)
s はアクチュエータ a を呼び出す
return(s)
ステートメント s は復帰文
write(s, v)
ステートメント s はシンボルv に書き込む
read(s, v)
ステートメント s はシンボルv を参照する
defuse(s, dv, sv)
ステートメント s で，シンボル dv への書き込みがシンボル sv を用いて行われる
controlFlow(a, g, s)
a 以下の制御フロー上で，ステートメント g はステートメントs から到達可能
dataFlow(a, d, dv, s, sv)
a 以下のデータフロー上で，ステートメント d 内のシンボル dv は，ステートメント s 内
のシンボル sv から到達可能

equal(x, y)
その他
x と y が等しい
true
真
false
偽
18
契約による検証
契約テンプレート

本研究は，典型的なリファクタリングパターンに
対して，契約をテンプレートという形で提供する
– AOリファクタリングカタログの各パターンに対して，
リファクタリングの前後で成立すべきプログラムの構
造的性質を契約としてまとめる
– COW言語で記述する
19
契約による検証
例に対する契約テンプレート
Move Method from Class to Inter-type

事前条件
1. メソッド<M>は，クラス<C>に定義されている
class(type: <C>) && owner(actuator: void <C>.<M>, type: <C>)
2. メソッド<M>は，アスペクト<A>に定義されていない
aspect(type: <A>) && !owner(actuator: void <C>.<M>, type: <A>)

事後条件
1. メソッド<M>は，クラス<C>に定義されていない
class(type: <C>) && !owner(actuator: void <C>.<M>, type: <C>)
2. メソッド<M>は，クラス<C>へインタータイプ宣言によって追加定義される
class(type: <C>) && intertypeOwner(actuator: void <C>.<M>, type: <C>)
3. メソッド<M>は，アスペクト<A>に定義されている
aspect(type: <A>) && owner(actuator: void <C>.<M>, type: <A>)
20
契約による検証
例に対する契約テンプレート
Move Method form Class to Inter-type
事前条件
contract {
requires (
class(type: <C>) && owner(actuator: void <C>.<M>, type: <C>) &&
}
);
aspect(type: <A>) && !owner(actuator: void <C>.<M>, type: <A>)
contract {
ensures (
}
);
条件1
条件２
事後条件
class(type: <C>) && !owner(actuator: void <C>.<M>, type: <C>) &&
intertypeOwner(actuator: void <C>.<M>, type: <C>) &&
aspect(type: <A>) && owner(actuator: void <C>.<M>, type: <A>)
条件1
条件２
条件３
21
契約による検証
契約による検証

リファクタリングを行う目的にあわせて，カタログから対
応するリファクタリングパターンを選択する

リファクタリングパターンの契約テンプレートを参照し，
<C>，<A>，<M>などのパラメータを実際のプログラムの
クラス名、アスペクト名，メソッド名で書き換えて，プログ
ラムに対応する契約を作成する

契約の事前条件とリファクタリング前のプログラムをペ
アとし，事後条件とリファクタリング後のプログラムをペ
アとして，それぞれ検証を行う
22
契約による検証
例に対応する契約
contract {
requires(
class(type: Queue) &&
owner(actuator: void Queue. display (), type: Queue) &&
aspect(type: Debugging) &&
!owner(actuator: void Queue. display (), type: Debugging)
);
}
contract {
ensures(
class(type: Queue) &&
!owner(actuator: void Queue. display (), type: Queue) &&
intertypeOwner(actuator: void Queue. display (), type: Queue) &&
aspect(type: Debugging) &&
owner(actuator: void Queue. display (), type: Debugging)
);
}
23
評価
24
①
AOリファクタリングカタログの内，
７８％パターンが契約テンプレート
を用いて検証することができる
–
②
Extract Inner Class to Standalone
◎
Inline Class within Aspect
◎
Inline Interface within Aspect
◎
Move Field from Class to Inter-type
◎
Move Method from Class to Inter-type
◎
Replace Implements with Declare Parents
◎
Split Abstract Class into Aspect and Interface
○
Introduce Aspect Protection
Replace Inter-type Field with Aspect Map
○ ：いくつか“◎”パターンを組み
Replace Inter-type Method with Aspect Method
◎
Tidy Up Internal Aspect Structure
記号なし：契約テンプレートを用意
Extract Superaspect
○
していないパターン
Pull Up Advice
◎
Pull Up Declare Parents
◎
Pull Up Inter-type Declaration
◎
Pull Up Marker Interface
◎
Pull Up Pointcut
◎
Push Down Advice
◎
Push Down Declare Parents
◎


○
Generalize Target Type with Marker Interface
合わせて検証できるパターン
–
Extract Feature into Aspect
Extend Marker Interface with Signature
◎ ：契約テンプレートを用意した
パターン
–
◎
Extract Fragment into Advice
評価

Change Abstract Class to Interface
動的特徴を記述することができる
契約テンプレートは，簡単に利用
できる
③
Push Down Inter-type Declaration
Push Down Marker Interface
Push Down Pointcut
◎
25
◎
◎
関連研究
26
関連研究

Refactoring object-oriented frameworks - W. F. Opdyke
– オブジェクト指向リファクタリングの正しさを一階述語論理を用いて検証する方
法を提案している
– 事前条件の概念を導入し，構造に関する26個の基本変換，３つの複合変換で
リファクタリングを表現する

Refactoring: Improving the Design of Existing Code - M. Fowler
– 複雑なリファクタリングをいくつか小さいリファクタリングに分けて検証する方法
を提案している
– 検証の順番とタイミングを決めるのが難しい

Deriving Refactorings for AspectJ - Leonardo Cole
– アスペクト指向リファクタリングを”laws”と呼ばれる変換規則を合成して行う方
法を提案している
27
まとめ
28
まとめ


本研究は，AOリファクタリングの正しさを契約に基づい
て検証する手法を提案した
AOリファクタリングカタログの各パターンに対応する契
約記述をテンプレートという形で提供した

各テンプレートは，実際にリファクタリングの検証のた
めに利用できることをテストし，有効であることを示した

今後は，契約テンプレートをサポートする検証ツールを
開発し，検証を自動化して行く必要がある
29
終わり
30

Download Report