Coq Party - rfなブログ11/27 に、Coq Partyに参加してきました。 資料などはこちら。 エンジニア・ミーツ・Coq すぐ分かる形式手法 形式手法とは？ 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法 仕様化の正しさは終盤のシステムテストまで分からない 結合テストでバグが「こんにちは！」 手戻りコストがとても大きい V字モデルは横軸工程、縦軸は「開発の詳細さのレベル」 ソフトウェア開発の不具合の半数は上流工程 その半分は下流工程まで見つからない 上流時点で「厳密で、間違い、漏れ、抜け、矛盾の無い仕様」が必要 仕様は自然言語で書かれているため、あいまい or/xor 問題や、if/iff 問題 など 自然言語ではなく、形式的な仕様記述が必要 形式手法 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う 数学ベースの厳密な定義 形式仕様は仕様の記述の形式化 プログラムではな
