ホーア／フロイト論理はどうよ？　preconditionやらpostconditionやら
invariant conditionやら、すべて記述するのはｶﾅｰﾘ面倒だが。