技術的に実装できそうな見通しは立っています。 postは関数呼び出し前にコールスタックを１つ分用意し、old-valueを退避させています。それと同じ要領で、代入文を実行する前に似たものを用意し、old-valueを退避させます。そして代入後にinvを評価します。…

以前から、不変条件にold-valueが使えると状態遷移が記述できる、と考えてました。 ところが、最初の代入時にはまずいことに気がつきました。 そのときは、old-valueは存在しないのです。 で、初期状態を表す新しいキーワードを追加します。 仮に INIT とし…