プログラム定理証明 - 有限会社ITプランニング(IT Planning Inc.)プログラム定理証明 弊社での、プログラム定理証明を用いたソフトウェア品質保証の取り組みについて紹介します。 iZE Smart Desktopミドルウェアの正しさ検証 (ソフトウェア科学会PPL2010においてポスター発表、TPP10にて発表) (有)ITプランニングは(株)アイズの「スマートデスクトップ・クライアント」の一部モジュールを請負開発し，その際証明支援器Coqを使用した． 本プロジェクトではD-Busで扱うデータとJSONとの相互変換に関して静的検証を行った． 具体的には，検証対象とする関数をCoqで定義した上で諸性質を証明し，Extract機能により全体のOCamlのプログラムと協調させるという方法を用いた． 今回行った検証の詳細と，実際にCoqを開発現場で使う上で行った工夫などを報告する． (PPL2010予稿集より) プログラム定理証明って？ プログラム定理証明は、プログ
