In article <82020020313172606cv8t-hdk / asahi-net.or.jp>,
  HIDAKA Takahiro <cv8t-hdk / asahi-net.or.jp> writes:

>  入れ子になっている場合などで、複数の invariant 検出を
> 書きたい場合に困らないんでしょうか。余計に見えてもひとつ
> オブジェクトがあったほうが楽なような気がするんですが。

あるのはかまいません、というか必要だと思いますが、それをプログラマに書
かせたくないわけです。そのうえで、入れ子だろうが再帰だろうが困らずに扱
えるような loop_variant が記述可能かどうか、というのが疑問なんです。
-- 
[田中 哲][たなか あきら][Tanaka Akira]
「ふえろ! わかめちゃん作戦です$(C⊇」(Little Worker, 桂遊生丸)