形式手法
formal methods
ソフトウェア
やシステムの
設計
・開発・分析のために形式的（数学的または論理的な）な記述やモデルを使用するアプローチ全般を指す
設計から仕様化、検証、テストなどソフトウェア開発のライフサイクル全般で活用される
生成AI
との相性も良い
AIと共に進化する開発手法：形式手法と関数型プログラミングの可能性
https://gyazo.com/d8e9d152661958fbfa1a6fa4a79d8cea
自動証明手法
定理証明
: e.g.
Lean
モデル検査
: e.g.
Alloy
、
TLA+
代表的なツール・技法
Alloy
:
関係モデル
を用いたシステム設計と分析のためのツール
TLA+
: 時間論理をベースにしたシステム設計と検証のための
フレームワーク
Z 言語
: ソフトウェア仕様の記述に使われる形式的な
仕様記述言語
B method
: システムの仕様から正確な実装を生成する
方法論