この記事は ryota2357 Advent Calendar 2024 の 10 日目の記事です。
今日の「ソフトウェア工学」という授業で Alloy の話が出た。せっかくなので少し触ってみた。
「alloy 形式手法」で検索したら次の記事が見つかったのでこれに沿ってやった。少しだけ記事の通りにいかないところがあったのでそれについて書く。
Alloy のインストールは brew install --cask alloy でできた。立ち上げるとこんな感じ
まず初めの sig A からやっていこうと思ったのだけど、Visualizer が開かなかった。Option から Visualize automatically を Yes にする必要があった。あと sig Stack の時に univ というものを使うのだけど、これを使って実行するためには Allow warnings も Yes にする必要があった。
その後は順調に Stack のモデルを作っていけたが、最後の Push pred を作るところでエラーが出た。
多分 version 5 -> 6 で何かあったのだろうと思い (設定で何かできたのかもしれないが) s' じゃなくて ss にすることで対処した。
「ソフトウェア工学」の授業では期末レポートで Alloy をやるらしいので、適当な時間でチュートリアルとかをやっておきたい。