概要: 本稿では，共通問題である在庫管理プログラムの仕様をAlloyのモデルとして記述したケーススタディについて報告する． モデル記述にあたっては，事前に記述していたJMLによる契約をリファレンスとした． Alloy Analyzerでの検証とともに，JMLによる記述との比較を行い， Alloyの記述，Alloy Analyzerのモデルファインダーとしての能力についてこの事例研究を通じての有効性を示す． タグ: alloy, analyzer, case, management, program, study, verification, warehouse

@inproceedings{森恵弥佳2013,
  author = {森 恵弥佳 and 岡野 浩三 and 楠本 真二},
  title = {在庫管理プログラムに対する Alloy Analyzer を用いた検証事例},
  booktitle = {情報処理学会シンポジウムシリーズ ウィンターワークショップ2013・イン・那須},
  volume = {2013},
  number = {1},
  pages = {5--6},
  year = {2013},
  month = {jan}
}