形式手法
formal method
ソフトウェア開発や仕様定義を数学的に厳密に効率的に行うための手法
具体的な実践的なユースケースは仕様記述、開発、検証など
参考
ソフトウェア開発の開発のフェーズ
仕様
厳密でかつ抽象的な数学的表現
このままでは実行できない
この段階で間違いを見つけられるのが嬉しい
解の記述
手軽に使えてある程度安全性を保てる奇跡のようなバランスに位置する
Isabelleなどの証明と異なり自動的に調べられる、人間の手を介さなくていい
設計
数学的検証が可能
解の記述
実装
数学的検証が可能
マジの実装
手続き的なプログラムのコードそのもの
関連
参考