仕様記述による静的検証

http://d.hatena.ne.jp/a-san/20060219#p1
の続き。
検証条件をいちいち人間が確認するのは面倒。
なので、検証条件の中に現れる変数に適当な値をぶち込んで、条件が成り立つかどうかを自動的に試せるようにした。以下は、検証条件の中に変数が３つあるので、それぞれを０〜２０まで変化させながら式が成り立つかどうかを調べた。この場合は２０＊２０＊２０＝８０００パターンを自動的に確認してます。
これで検証したことにはならないけれど、反例を探すのに役立ちそう。

検証条件 (1 <= i and i <= (N + 1) and f = ! (i + -1) and i > N) ⇒ f = ! N
   変数試験範囲[id="i" min=0 max=20]
   変数試験範囲[id="f" min=0 max=20]
   変数試験範囲[id="N" min=0 max=20]
   指定範囲内では成立