言語仕様の拡張案

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

class エレベータ

types
-- エレベータは<上昇>からいきなり<下降>になることはない。
-- 必ず<停止>し（ドアが開き利用者の出入りを行った後）<上昇>、
-- または<下降>する。
public 方向型 = <上昇> | <下降> | <停止>
    inv d ==
        (d~ = INIT => d = <停止>) and
        ((~d <> d) =>
            (d~ = <停止> => d = <上昇> or d = <下降>) and
            (d~ = <上昇> => d = <停止> ) and
            (d~ = <下降> => d = <停止> ));

end エレベータ

最初は新しいキーワードを追加することに躊躇したけれど、
RESULTだって、postでしか使えないキーワードです。
新しいキーワードを追加することで、状態遷移を記述できるなら、
ためらう必要はない。