形式手法がわからない
詳しい人に聞きたいmrsekut.icon
形式手法と定理証明の違いや関係
Z, Alloy, VDMあたりは形式仕様記述言語と紹介されることが多い
一方で、Agda, Coq, Isabelle, Lean等は別の括りとして扱われているように見える
が、その違いがわからない
言語の目的としてそもそも違うのか、どれぐらい違うものなのか、両立するのか、等々が全然わからない
このプロジェクト上の揺れてる用語をwikipediaを参考に統一するかmrsekut.icon
定理証明→自動定理証明？
形式検証→形式的検証
形式手法
以下の4つほどの言語がどういう立ち位置なのか気になる
最近よく見かける4つmrsekut.icon
形式手法と定理証明がどのぐらい違うものなのか、どういう関係性なのかもよく分かっていない
この辺は具体例に触れながら徐々に学んでいくしか無いと思ってるmrsekut.icon
あまりにもその辺の分野の概観がわからないので
まず軸となる比較対象を作る必要がありそう
資料が多かったりするのでいったんAlloyをやってみようと思うmrsekut.icon
Alloyを軸に形式手法のノリが分かってきたら、他の言語も見てみて、拡げたい
まあそもそもmrsekut.iconがしたいのは形式手法ではなく、「抽象化」に対する嗅覚を養うことなので、そこはブレさせないように注意が必要
形式手法の知識はついでに知れると嬉しい
あわよくば業務に導入したい