概要: 近年，契約に基づく設計による開発手法が脚光を浴びている．これを実現する言語の一つとしてJMLが挙げられる．本研究では、プログラム設計の共通問題である酒屋の在庫管理問題に対してJMLを用いて仕様作成を行いプログラムを記述し，ESC/Java2を用いて実際に検証を行った．本報告では, この過程で得られた知見(作業量, 現バージョンのESC/Java2の記法の問題点, 解決法など)について報告する．また，ソフトウェア開発にJMLを用いる上での課題について考察する. タグ: case, study, ―, design, warehouse, management, program, jml, verification, esc/java2, ―

@inproceedings{尾鷲方志2007a,
  author = {尾鷲 方志 and 岡野 浩三 and 楠本 真二},
  title = {JMLを用いた在庫管理プログラムの設計とESC/Java2 を用いた検証},
  booktitle = {電子情報通信学会技術報告},
  volume = {107},
  number = {176},
  pages = {37--42},
  year = {2007},
  month = {aug}
}