前回触れたiContractやJMLでは、クラスやメソッドの定義の直前にドキュメンテーション・コメントと同じようにして契約を書けます。ところが、アスペクトを使う場合には、ソースコード内に直接契約を埋め込むことはできません。契約だけ別ファイルに書くことになります。これは欠点でもありますが、契約だけを事前に準備する(契約ファースト!)には向いているし、契約(だけ)のメンテナンスも楽です。 そういう事情で、ここでは、インターフェースに契約を付与することを考えましょう。 契約付きインターフェース 契約付きインターフェースの構文は、Eiffelを参考にテキトーにでっち上げます。 クラス宣言頭部に不変条件を、invariant 条件の形で書く。 メソッド宣言頭部に事前条件を、requires 条件の形で書く。 メソッド宣言頭部に事後条件を、ensures 条件の形で書く。 戻り値はresultで表す。