概要: ソフトウェア開発の重要概念である契約による設計（Design by Contract，以下DbCとする）では，各クラス・メソッドが満たすべき仕様を表明として明確に定義することでソフトウェアの仕様理解の補助や，プログラム検証を可能にする．また表明の記述が十分であれば，メソッドの使用者が実装の詳細を考慮する必要がなくなり，情報隠蔽の度合いやモジュール性を高めることができる．DbCを実現するための具体的な言語として，Javaのソースコード中に表明を記述するためのJML（Java Modeling Language）などが存在する．また，オブジェクト指向モデリングに影響を受けた形式仕様記述言語としてAlloyが存在する．Alloyは自動解析ツールAlloy Analyzerを備えており，記述したモデルに対して表明の検証を行うことができる． 本研究では，JMLで記述された表明に関する欠陥を検出あるいは発見しやすくする手法を提案する．この手法は二つの要素からなっている．一つ目は，洗練の程度を可視化することで洗練の不十分さを使用者に発見しやすくするものである．まず，手動でJMLをAlloyに変換する．そのAlloy記述を使用して，メソッドの表明が全て満たされたときのオブジェクトの例をAlloy Analyzerを用いてグラフとして出力する．二つ目は，実装と表明との不一致を検出するものである．まず，手動でJMLとJavaで書かれたソースコードをAlloyに変換する．そのAlloy記述を使用して，メソッドの実装が表明を満たさないときのオブジェクトの例をAlloy Analyzerを用いてグラフとして出力する． 適用実験はソフトウェア開発のための古典的な共通問題である在庫管理プログラムに対して行った．このプログラムは過去に研究グループが作成したものであり，Javaで記述されている．またJMLによる表明も付与されている．実験の結果，8ヶ所の表明に関する欠陥を検出することができ，手法の有用性を確認できた．また，今回の手法では対応できなかったJMLおよびJavaの構文，Alloy Analyzerの解析の制限や記述および検証にかかるコストについても考察した． タグ: alloy, JML

@mastersthesis{森恵弥佳2013a,
  author = {森 恵弥佳},
  title = {JMLによる仕様記述に対するAlloy Analyzerを用いた 検証手法の提案—在庫管理プログラムに対する適用—},
  school = {大阪大学},
  type = {Bachelor's Thesis},
  year = {2013},
  month = {feb}
}