契約に基づいたアスペクト指向リファクタリングの検証 九州工業大学大学院 情報工学研究科　　 朴　金姫，篠塚 卓，鵜林　尚靖

発表の流れ 背景 アスペクト指向プログラミング（AOP） AOリファクタリング 契約による検証 評価 関連研究 まとめ

アスペクト指向プログラミング（AOP） AOリファクタリング 背景 　アスペクト指向プログラミング（AOP） 　AOリファクタリング

アスペクト指向プログラミング（AOP） AOPは横断的関心事を分離し，アスペクトとしてモジュール化する技術である 横断的関心事：様々なクラスに散在している関心事 アスペクト：横断的関心事をモジュール化する単位 ウィーバーによってシステム本来の機能に織り込まれる AspectJ：代表的なAOP言語 アプリケーション機能実装 アプリケーション機能 アスペクト ウィーバー アスペクト

横断的関心事 ログ処理の例 赤い線はログ処理を行うコード 複数の場所に分散している AOP AspectJ. http://eclipse.org/aspectj/

横断的関心事 AOP 実際の振る舞い クラス ・・・・・・ アスペクト ・・・・・・ methoda methoda Advice1 織り込み method1 methodb method2 Advice2 methodc methodb method2 methodc ・・・・・・ method1 ・・・・・・

AspectJ アスペクト ： AspectJ中のモジュール単位の一つ AOP AspectJ アスペクト ： AspectJ中のモジュール単位の一つ ジョインポイント : プログラムが実行する時に割り込ませるコードの位 置 メソッドの呼び出し先 ポイントカット : 織り込み先のジョインポイントを選択する記述 プリミティブポイントカット：call , execution etc. ポイントカット中のジョインポイントは &&, ||, ! などの論理記号で組み合わせる アドバイス : 指定するポイントカットによって選択されるジョイン ポイントに差しかかったときに実行されるコード 実行するタイミングによってbefore，after, around などがある ウィーバー : クラスとアスペクトを織り合わせる処理系

AspectJの例 AOP 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();　} }

リファクタリング リファクタリング AOリファクタリング プログラムの外部的振る舞いを変えず，内部構造を改善する手法である リファクタリングを行った後，プログラムコードの理解や修正が簡単になる AOリファクタリング アスペクト指向におけるリファクタリング

AOリファクタリングカタログ Catalog of Aspect-Oriented Refactorings --Monteiro, M. P. ①横断的関心事を抽出するためのリファクタリング ②アスペクト内部を再構造化するためのリファクタリング ③一般化を行うためのリファクタリング

例に関するリファクタリングパターン リファクタリングパターン名： 典型的な状況： 推奨動作 AOリファクタリング 例に関するリファクタリングパターン リファクタリングパターン名： Move　Method from Class to Inter-type 典型的な状況： あるメソッドが含まれている関心事はクラスの関心事ではない 推奨動作 そのメソッドをアスペクトへインタータイプとして移動する

例におけるリファクタリング Move Method from Class to Inter-type AOリファクタリング class Queue { 　void enqueue (Object element) {…} 　Object dequeue () {…} 　boolean empty () {…} 　int size () {…} 　　．．．．．． } aspect Debugging{ class Queue { 　void enqueue (Object element) {…} 　Object dequeue () {…} 　boolean empty () {…} 　int size () {…} 　　．．．．．． void display () { 　　　Iterator i = elements.iterator (); 　　　　．．．．．． } Queue.display (){ ．．．．．． } } aspect Debugging{ ．．．．．．

リファクタリングで発生する問題 Move Method from Class to Inter-type AOリファクタリング class Queue { 　void enqueue (Object element) {…} 　Object dequeue () {…} 　boolean empty () {…} 　int size () {…} 　　．．．．．． } aspect Debugging{ class Queue { 　void enqueue (Object element) {…} 　Object dequeue () {…} 　boolean empty () {…} 　int size () {…} 　　．．．．．． void display () { 　　　Iterator i = elements.iterator (); 　　　　．．．．．． } void display () { 　　　Iterator i = elements.iterator (); 　　　　．．．．．． } ．．．．．． } } aspect Debugging{ ．．．．．． void display () { 　　　Iterator i = elements.iterator (); 　　　　．．．．．． }

解決方法 契約：静的な構造に関する性質を表現する リファクタリングを行った後プログラムの構造は変わるが振る舞いが変わってはいけない AOリファクタリング 解決方法 リファクタリングを行った後プログラムの構造は変わるが振る舞いが変わってはいけない リファクタリングを行う最中に発生する問題は発見しにくい リファクタリングの正しさを検証する ①振る舞いが正しく保存される ②構造が正しく変換される 契約：静的な構造に関する性質を表現する

契約による検証

契約 リファクタリングを行う前後で満たされるべきプログラムの構造的性質を事前条件，事後条件として与える．これらの条件をまとめて，契約と呼ぶ． 契約による検証 契約 リファクタリングを行う前後で満たされるべきプログラムの構造的性質を事前条件，事後条件として与える．これらの条件をまとめて，契約と呼ぶ． 事前条件：リファクタリングを行う前，プログラムの性質 事後条件：リファクタリングを行った後，プログラムの性質 COW（COntract Writing language）言語で記述する プログラムの静的な構造や振る舞いを一階述語論理で記述する

COWの基本述語① 構造的特徴を表す述語 契約による検証 class(c) クラス interface(i) i はインターフェース extends(x, y) 継承関係を表す implements(x, y) 実装関係を表す constructor(a) コンストラクタ method(a) メソッド field(v) フィールド enumerator(v) 列挙子 parameter(v) フォーマルパラメータ variable(v) アクチュエータの局所変数 name(x, n) 名前を表現する body(a, b) アクチュエータ のボディトークン列 abstract(x) 修飾子 abstract によって修飾される owner(x, t) 所有関係 aspect(a) アスペクト pointcut(p) ポイントカット beforeAdvice(a) before アドバイス afterAdvice(a) after アドバイス aroundAdvice(a) around アドバイス intertypeOwner(x, c) 織り込みによる所有関係 target(a) 制約条件の適用先アクチュエータ source(a) 織り込まれるアドバイス

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 偽

契約テンプレート 本研究は，典型的なリファクタリングパターンに対して，契約をテンプレートという形で提供する 契約による検証 契約テンプレート 本研究は，典型的なリファクタリングパターンに対して，契約をテンプレートという形で提供する AOリファクタリングカタログの各パターンに対して，リファクタリングの前後で成立すべきプログラムの構造的性質を契約としてまとめる COW言語で記述する

例に対する契約テンプレート Move Method from Class to Inter-type 契約による検証 事前条件 2. メソッド<M>は，アスペクト<A>に定義されていない 事後条件 1. メソッド<M>は，クラス<C>に定義されていない 2. メソッド<M>は，クラス<C>へインタータイプ宣言によって追加定義される 3. メソッド<M>は，アスペクト<A>に定義されている class(type: <C>) && owner(actuator: void <C>.<M>, type: <C>) aspect(type: <A>) && !owner(actuator: void <C>.<M>, type: <A>) class(type: <C>) && !owner(actuator: void <C>.<M>, type: <C>) class(type: <C>) && intertypeOwner(actuator: void <C>.<M>, type: <C>) aspect(type: <A>) && owner(actuator: void <C>.<M>, type: <A>)

例に対する契約テンプレート 事前条件 事後条件 契約による検証 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>) 　　); } ensures ( 　　　　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 条件２ 事後条件 条件1 条件２ 条件３

契約による検証 リファクタリングを行う目的にあわせて，カタログから対応するリファクタリングパターンを選択する リファクタリングパターンの契約テンプレートを参照し，<C>，<A>，<M>などのパラメータを実際のプログラムのクラス名、アスペクト名，メソッド名で書き換えて，プログラムに対応する契約を作成する 契約の事前条件とリファクタリング前のプログラムをペアとし，事後条件とリファクタリング後のプログラムをペアとして，それぞれ検証を行う COW言語はツール化されている．契約と検証対象のプログラムあれば，検証処理は自動化にできる．

例に対応する契約 契約による検証 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) 　　); }

評価

評価 AOリファクタリングカタログの内，７８％パターンが契約テンプレートを用いて検証することができる 契約テンプレートは，簡単に利用できる ① Change Abstract Class to Interface ◎ Extract Feature into Aspect ○ Extract Fragment into Advice 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 ② Extend Marker Interface with Signature Generalize Target Type with Marker 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 Push Down Inter-type Declaration Push Down Marker Interface Push Down Pointcut 評価 AOリファクタリングカタログの内，７８％パターンが契約テンプレートを用いて検証することができる ◎ ：契約テンプレートを用意したパターン ○ ：いくつか“◎”パターンを組み合わせて検証できるパターン 記号なし： 契約テンプレートを用意していないパターン 動的特徴を記述することができる 契約テンプレートは，簡単に利用できる 記号なし，

関連研究

関連研究 Refactoring object-oriented frameworks - W. F. Opdyke オブジェクト指向リファクタリングの正しさを一階述語論理を用いて検証する方法を提案している 事前条件の概念を導入し，構造に関する26個の基本変換，３つの複合変換でリファクタリングを表現する Refactoring: Improving the Design of Existing Code - M. Fowler 複雑なリファクタリングをいくつか小さいリファクタリングに分けて検証する方法を提案している 検証の順番とタイミングを決めるのが難しい Deriving Refactorings for AspectJ - Leonardo Cole アスペクト指向リファクタリングを”laws”と呼ばれる変換規則を合成して行う方法を提案している

まとめ

まとめ 本研究は，AOリファクタリングの正しさを契約に基づいて検証する手法を提案した 各テンプレートは，実際にリファクタリングの検証のために利用できることをテストし，有効であることを示した 今後は，契約テンプレートをサポートする検証ツールを開発し，検証を自動化して行く必要がある

終わり