仕様記述による静的検証

http://dontaku.csce.kyushu-u.ac.jp/books/ProgramSpecification/
IT Text　プログラム仕様記述論
を見ながら、静的検証を行うプログラムを作ってみました。
プログラムと、事前条件＋事後条件＋ループ不変条件を設定すれば、検証条件を出力します。
言語体系がシンプルなので構文木は簡単に作れるのですが、パターンをバインドするのが難しい。（←言葉の使い方、あってるのかな？）多分、prolog的な仕組みが必要なんだけど、自分で作っておきながら、何で動くのかわからない。ｗ
あと、出力された検証条件が冗長なので簡略化する処理を入れたのだけれど望む形にするのは大変。

{N >= 0}
検証条件{N >= 0 ⇒ 1 <= N + 1}
i := 1;
f := 1;
{(1 <= i and i <= N + 1 and f = ! (i - 1))}
While i <= N Do
検証条件{(1 <= i and i <= N + 1 and f = ! (i - 1) and i <= N) ⇒ (1 <= i + 1 and i + 1 <= N + 1 and f * i = ! (i + 1 - 1))}
f := f * i;
i := i + 1
End
検証条件{(1 <= i and i <= N + 1 and f = ! (i - 1) and i > N) ⇒ f = ! N}
{f = ! N}

赤字が出力された検証条件。階乗のプログラム。