SWETの仕様分析サポートチーム所属のtakasek(@takasek)です。 仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています(形式手法 カテゴリーの記事一覧)。 当記事は、Kuniwak(@orga_chem)により社内開催されたAlloyガイダンスを元に再構成した記事です。よく知られたデータ構造であるStackを形式仕様記述しビジュアライズすることで、Alloyの使い方と利点を実感できます。Alloy未経験者でもステップバイステップで試せるように構成しました。是非、お手元にAlloyをインストールして読み進めてください。環境はAlloy 5.1.0を想定しています。 https://github.com/AlloyTools/org.alloytools.alloy/release
![形式手法でデータ構造を記述・検査してみよう:Alloy編 - DeNA Testing Blog](https://cdn-ak-scissors.b.st-hatena.com/image/square/14ea016ccd489bf963af6a8665956f32f3f2f352/height=288;version=1;width=512/https%3A%2F%2Fcdn-ak.f.st-hatena.com%2Fimages%2Ffotolife%2Fs%2Fswet-blog%2F20200501%2F20200501184101.png)