事後条件で@pre(アサーションをアスペクト&メタデータで実装)

事後条件では，メソッドが実行した後のあるべき状態(引数や戻り値，自身のフィールドの値など)を記述します．
この場合，メソッドが実行する前の状態を参照できないと，うまく表明を記述できない場合があります．
そこでEiffelではold，OCLでは@preを指定することができます．
例えばカウンタのinc()メソッドの場合，

count = count@pre + 1

という具合に記述することで，カウンタの値がメソッドの実行前よりも1だけ増加しているべきだということを表明しています．素晴らしい．
素晴らしいことは確かなのですが，これを効果的に実装することはなかなか大変そうです．
まず，プリミティブ型の引数やフィールドは問題ありません．メソッドの実行前に，それらのコピーをとっておけばいいだけです．
しかし，参照型の引数やフィールドの場合は悩ましくなってきます．
例えばリスナーを追加するaddListener(Listener)というメソッドの場合．

listenres.size = listeners.size@pre + 1

みたいな事後条件を書きたくなるわけですが，この場合はlistenersというオブジェクトへの参照をコピーしてあっても意味がありません．メソッドの実行後でも，参照しているオブジェクトは同じですからね．listenersが参照しているオブジェクトのコピーが必要になるわけです．
ですが，参照型のオブジェクトが全てCloneableではないですし，場合によっては引数やフィールドで参照しているオブジェクトのフィールドが参照しているオブジェクトのコピーが必要になるかもしれません．うーむ．
妥協案としては，引数やフィールドが参照型で，その型がColneableをimplementsしていたらclone()する，そうでなければ参照をコピーしておく，かなぁ．
それで，フィールドのコピーをMapに入れて，それをthisという名前でMapに入れて，それをpreという名前でBindingに突っ込んであげれば，

 * @@Ensure("size", "this.listener.size() == pre.this.listeners.size() + 1")

みたいにできるらしい．Mapのエントリをプロパティ風に使えちゃうのね．いいなぁ，Groovy．