文献

J-GLOBAL ID：201302264460799882   整理番号：13A1386781

ソースコードからの仕様発掘技術

Specification Mining Technology for Automatically Inferring Software Specifications from Source Code

著者 (3件)： 今井健男 (東芝) ,  酒井政裕 (東芝) ,  岩政幹人 (東芝)
資料名： 東芝レビュー  (Toshiba Review)
巻： 68  号： 8  ページ： 35-38  発行年： 2013年08月01日 
JST資料番号： F0360A  ISSN： 0372-0462  CODEN： TORBA  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ソフトウェアの派生開発を効率的に行うには,仕様とプログラムの対応が維持されていることが重要である。東芝は,プログラムのソースコードから仕様情報を発掘し,それを仕様へ反映するための技術開発を行っている。仕様に相当する情報をプログラムから機械的に発掘し抽出できれば,今後の製品展開で有用な情報を効率的に洗い出し,設計書を常に最新の状態に保つことができる。今回,その取組みの一環として,プログラムが正しく動作するための前提と仮定している条件(事前条件)を仕様としてプログラムから自動推定するための新たな技術を開発した。この技術を用いてC言語向けに試作したツールを例題プログラムに適用し,この技術が実用的で,人が考えるのと同等以上に汎用的な仕様を得ることができ,この技術の実用性を確認できた。(著者抄録)

シソーラス用語： *計算機コード ,  *仕様 ,  C言語 ,  推定
準シソーラス用語： ソースコード ,  *仕様発掘 ,  自動推定

分類 (1件)： 計算機システム開発  (JD02010R)

引用文献 (8件)：

• (1) Meyer, B. Object-Oriented Software Construction. USA, Prentlce-Hall, Inc.,1988, 534p.
• (2) 酒井政裕 他. データ構造に関する仕様を含め検証できるC言語プログラム部品検証ツール CForge. 東芝レビュー. 64, 8, 2009, p.20-23.
• (3) Sakai, M. et al. "Model-checking C programs against JML-like speciflcation language". Proceedings of the 19th Asia-Pacific Software Engineering Conference (APSEC2012).Hong Kong, 2012-12, IEEE/ACM. p.174-183.
• (4) Jackson, D. 抽象によるソフトウェア設計-Alloyではじめる形式手法.東京, オーム社, 2011, 368p.
• (5) Liffiton, M.; Sakallah, K. Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Journal of Automated Reasoning. 40, 1, 2008, p.1-33,

タイトルに関連する用語 (2件)： ソース ,  仕様