オブジェクトにそのアノテーションを持たせて
DbCのinvariantととしてメソッド前後毎回チェックすればええ。