ソフトウェア開発や仕様定義を数学的に厳密に効率的に行うための手法

形式仕様記述言語で仕様を厳密に書き、それを論証できる

具体的な実践的なユースケースは仕様記述、開発、検証など

参考

ソフトウェア開発の開発のフェーズ

仕様

厳密でかつ抽象的な数学的表現

このままでは実行できない

この段階で間違いを見つけられるのが嬉しい

解の記述

型システムは仕様の中でも大雑把な部類の仕様

手軽に使えてある程度安全性を保てる奇跡のようなバランスに位置する

Isabelleなどの証明と異なり自動的に調べられる、人間の手を介さなくていい

データフロー解析と似ているらしい

どのへんが #??

設計

数学的検証が可能

具体的にここはなに #??

解の記述

実装

数学的検証が可能

マジの実装

手続き的なプログラムのコードそのもの

関連

参考