メイヤー流契約に限らず、一般のホーア式もプログラムコードに翻訳する方法を考えてみました。特に、全称限量子（「すべての…に関して…」を意味する）の扱いを工夫してみます。（これは、「AspectJによる契約駆動開発」に関連したエントリーです。）明示的な…