こんにちは、チェシャ猫です。 Alloy は関係論理を用いた形式手法ツールの一種です。本記事では、2021 年 11 月にリリースされた Alloy 6 の新機能、Mutable Field を用いた検査について解説します。この機能を使用することで、時間発展するタイプのシステムをよりシンプルに記述できるようになりました。 なお、本記事は従来の v5 以前の Alloy に触ったことがある読者を想定しています。したがって Alloy のツールとしての位置付けや基本的な文法・機能については説明しません。興味のある読者には『抽象によるソフトウェア設計ーAlloy ではじめる形式手法』（以下 Jackson 本）をお勧めします。 それでは早速、Alloy 6 をダウンロードして始めましょう。 TL;DR Mutable Field が導入され、時刻に従って変化するような関係が記述可能になった それ