2024-03-30T13:13:37Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001743632023-11-14T00:51:14Z06164:06165:06522:08893
証明駆動開発の現実的な開発プロジェクトへの適用に向けてjpn開発支援・OSShttp://id.nii.ac.jp/1001/00174329/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=174363&item_no=1&attribute_id=1&file_no=1Copyright (c) 2016 by the Information Processing Society of Japan富士通研究所富士通研究所山本, 晃治宗像, 一樹形式的証明やそれに基づく証明駆動開発は工数増加の懸念から採り入れられないことが多い.しかし今回実験の過程で実プロジェクトで使用中のプログラムに対して,テストで見逃されていた潜在バグを発見した.これは形式的証明の有用性の一端を示すものである.本稿では,実業務での適用を念頭に,証明駆動開発をプログラムの動作保証に活用するための方法を提案する.実業務で稼働させるアルゴリズムに対して,その性質を Coq で形式的に証明し,証明済みプログラムを,通常の実業務でよく用いられる非関数型プログラム言語に変換するモジュールについて説明する.また関数型プログラム言語である Coq から非関数型プログラム言語 Python への変換結果のコード実行時のメモリ使用量の悪化を防ぐ方策を提示し,10 倍程度の悪化にまで抑えられることを示す.ソフトウェアエンジニアリングシンポジウム2016論文集20161041112016-08-242016-08-23