前回触れたiContractやJMLでは、クラスやメソッドの定義の直前にドキュメンテーション・コメントと同じようにして契約を書けます。ところが、アスペクトを使う場合には、ソースコード内に直接契約を埋め込むことはできません。契約だけ別ファイルに書くことになります。これは欠点でもありますが、契約だけを事前に準備する（契約ファースト！）には向いているし、契約（だけ）のメンテナンスも楽です。
そういう事情で、ここでは、インターフェースに契約を付与することを考えましょう。
契約付きインターフェース
契約付きインターフェースの構文は、Eiffelを参考にテキトーにでっち上げます。
- クラス宣言頭部に不変条件を、
invariant 条件の形で書く。 - メソッド宣言頭部に事前条件を、
requires 条件の形で書く。 - メソッド宣言頭部に事後条件を、
ensures 条件の形で書く。 - 戻り値は
resultで表す。 - メソッドに入る前の式の値は
old(式)で表す。 - コンストラクもnewという名前のメソッドとして記述できる。
例：
public interface Person
invariant getAge() >= 0
invariant getName() != null
{
new(String name, int age)
requires name != null
requires age >= 0;int getAge();
String getName();
void happyBirthday()
ensures getAge() == old(getAge()) + 1;
}
クラス不変条件の代わりに、メソッドの事後条件も使えます。
int getAge()
ensures result >= 0;String getName()
ensures result != null;
契約の表明とアクセッサ、その他の構文要素
契約（クラス不変条件、メソッド事前条件、メソッド事後条件）を記述する論理式を表明とも呼びます。表明はもちろん真偽値（boolean値）を値とする式ですが、表明に副作用があるとヤッカイです。よって、表明内で使用するメソッドは副作用がないものを使うべきです。
値はあるが、副作用がないメソッドをアクセッサとここでは呼びます。あるメソッドがアクセッサであることを、アノテーション@Accessorで示しましょう。これは（当面は）気休め（人間に対する注意・警告）です。メソッドがほんとにアクセッサであるかどうかを言語処理系が判断するのは困難ですから。ただし、あるアクセッサの実行によって、他のアクセッサの値が変化しないことを表明にすることはできます。
int getAge()
ensures getAge() == old(getAge())
ensures getName().equals(old(getName())) ;String getName()
ensures getAge() == old(getAge())
ensures getName().equals(old(getName())) ;
とりあえず今回は、@Accessorは気休めとして使います。
それと、表明に名前を付けたいときは invariant[NotNullName] getName() != nullのように、そしてエラーメッセージはコロンの後に書くことにします（assertの構文を拝借）。例えば、ensures getAge() == old(getAge()) + 1 : "Unexpected 'age' update."。
んで、構文要素がひととおり入るように（作為的な）変更をして：
public interface Person
invariant[NotNullName] getName() != null
{
new(String name, int age)
requires name != null : "Null name for constructor."
requires age >= 0; : "Negative age for constructor."@Accessor
int getAge()
ensures result >=0 && result < 150;@Accessor
String getName();void happyBirthday()
ensures[AgeUpdate] getAge() == old(getAge()) + 1
: "Unexpected 'age' update." ;
}
契約アスペクトを生成する
上に書いた契約付きインターフェースは、そのままではjavacはもとよりajcも理解できないシロモノなので、通常のインターフェースとアスペクトに分解します。次のような感じでしょう。
/* Person.java */public interface Person {
/* accessor */
int getAge();
/* accessor */
String getName();void happyBirthday();
}
以下、*Violationというruntime exceptionが定義されているとします。AspectJの解説は（今は）一切しません。
/* PersonContract.java */aspect PersonContract {
/*
* invariant[NotNullName] getName() != null
*/
after(Person person) :
execution(* Person+.*(..)) && !cflow(adviceexecution()) && this(person)
{
if (! (person.getName() != null)) {
throw new InvariantViolation("[NotNullName]@" + thisJoinPoint);
} else {
System.out.println("*** OK INV[NotNullName]@" + thisJoinPoint);
}
}/*
* new(String name, int age)
* requires name != null : "Null name for constructor."
*/
before(String name) :
execution(Person+.new(String, int)) && args(name, ..)
{
if (! (name != null)) {
throw new PreconditionViolation("Null name for constructor." +
" @" +
thisJoinPoint);
} else {
System.out.println("*** OK PRE@" + thisJoinPoint);
}
}/*
* new(String name, int age)
* requires age >= 0; : "Negative age for constructor."
*/
before(int age) :
execution(Person+.new(String, int)) && args(.., age)
{
if (! (age >= 0)) {
throw new PreconditionViolation("Negative age for constructor." +
" @" +
thisJoinPoint);
} else {
System.out.println("*** OK PRE@" + thisJoinPoint);
}
}/*
* int getAge()
* ensures result >=0 && result < 150;
*/
after() returning (int result) :
execution(int Person+.getAge()) &&
!cflow(adviceexecution())
{
if (! (result >= 0 && result < 150)) {
throw new PostconditionViolation("@" + thisJoinPoint);
} else {
System.out.println("*** OK POST@" + thisJoinPoint +
" returns " + result);}
}
/*
* void happyBirthday()
* ensures[AgeUpdate] getAge() == old(getAge()) + 1
* : "Unexpected 'age' update." ;
*/
int _old_getAge;
before(Person person) :
execution(void Person+.happyBirthday()) &&
!cflow(adviceexecution()) &&
this(person)
{
_old_getAge = person.getAge();
}
after(Person person) returning :
execution(void Person+.happyBirthday()) &&
!cflow(adviceexecution()) &&
this(person)
{
if (! (person.getAge() == _old_getAge + 1)) {
throw new PostconditionViolation("[AgeUpdate]" +
"Unexpected 'age' update." +
" @" +
thisJoinPoint);
} else {
System.out.println("*** OK POST[AgeUpdate]@" + thisJoinPoint);
}
}
}
「契約→アスペクト」の変換（翻訳）は機械的といえば機械的なのですが、僕は、その翻訳ルールを完全に把握しているわけではありません。そもそも、AspectJのcallとexecutionの使い分けとか、cflow、adviceexecutionの振る舞いとかも理解があやしい。
というわけで、もう少し調べたり、試したり、考えたりが必要ですね。続きはまたいずれ。（少しだけ続き書いた。）
