概要: ソフトウェアの開発において，従来から使われている手法としてV字型モデルによる設計法がある．このV字型設計法において，近年，Design by Contract(契約に基づく設計，以下DbCとする)による考え方が脚光を浴びている．DbCに基づいた開発では，アサーションにより契約を示す．アサーションを実現するための言語のとしてAlloyやJMLが挙げられる．Alloyは，Model Finderと呼ばれるAlloyAnalyzerを用いて，抽象度の高い設計において，仕様の矛盾発見などに役立つ．一方JMLは，Javaコードと結びついており，抽象度の低い段階での設計，実装の検証に役立つ．このため，AlloyからJMLに変換が可能ならば，抽象度が高く正当性のある程度保障された契約に対し，それ侵さぬよう低レベル設計が得られるため，より信頼性の高い開発を行うことができる． 本研究では，AlloyからJML付きのJavaのコードへの変換をすることを念頭において，そのための事例研究として，在庫管理プログラムの設計をAlloyとJMLで行った．それぞれAlloyAnalyzerとESC/Javaを用いてその正当性を検証した．また，各検証については，作成した在庫管理プログラムにおいて，警告内容について，なぜそのような警告がでたか，そして解決できたかについてまとめ考察した．結果，Alloyにおいては一部仕様を省略したがAlloyによる述語の扱い方を工夫することによりJMLと類似した記法により仕様記述をすることができた． タグ: case, study, design, warehouse, management, program, jml, alloy, verification, validation, tools

@mastersthesis{尾鷲方志2007,
  author = {尾鷲 方志},
  title = {仕様記述言語JMLとAlloy を用いた在庫管理プログラムの設計に対するモデル検査ツールによる検証事例},
  school = {大阪大学},
  type = {Bachelor's Thesis},
  year = {2007}
}