alloyを使ってみたい
まず、alloyについて調べる
日本語書籍読むかー？
table:形式手法
種類 説明 代表的な記述言語・ツール
形式仕様記述 矛盾がなく論理的に正しい仕様を作成する VDM++/Event-B/Z/Alloy etc.
モデル検査 プログラムの状態をモデル化することで、プログラムが期待される性質を満たすことを検証する Promela/TLA+ etc.
定理証明 法則や説明に基づき、理論的に性質が成り立つことを示していく Coq/Isabelle etc.
大雑把に３つあるっぽい
alloyとtla+の比較してる
大雑把に言うと、TLA+のほうがステートマシンの記述が楽かも
たとえば並行分散アルゴリズムの仕様化と検証とかがTLA+強いっぽい
自分が書くようなステートマシンは、そこまで遷移が複雑とは思えない
実際に書けばよくね、という気もする
また、ここを機械による支援で嬉しいのは、人間が把握できないくらいの量、規模のときな気がする
もちろん、そうでない小さい範囲でも自動的に検査できたら嬉しいんだろうが
から、モデル検査方面は一旦スルー
定理証明はそれはそれで面白そうだが、別トピックだろう
仕様の記述をして、
漏れを把握したり、
要するに、機械にデバッグをしてもらうという感じ
壁に一個ずつ体当りして、やべー条件を見つけてもらうみたいな
そもそも自分の認識やモデルの仕方がイケているかを考え直すのに使いたい
そう、本当はここがissueなはずなんだよな
alloyという言語を学んでも、集合や述語の書き方が下手だと、意味？がないはずだ
alloyについて
公式
自分の使い所があるのかを考える
自分で試す課題がほしい
SWETの記事にあったgitのcommitのやつ
tutorialの家のやつ
構文木, lambda calcのやつちょっと面白いが
推理系の例は面白い
code:als
abstract sig Person {
kill : this -> Person}
one sig A,B extends Person {}
fact{
}
これだけみても、
人は、死とnot死の２値であるのは本当か？
killは、事実なのか？
偶然死はどうするのか
https://gyazo.com/dfad29c5e9e7553e8f117938514e8b1b
a killls B, B kills Bの解釈は、協力なのか？
たとえば、
AがBをkillしたとBがBをkillする
BがBをkillしたあと、AがBをkillする
とか、解釈の余地がある
疑問が浮かぶ。で、それをさらにモデルに落とし込むと良いのだろう
レンタルシステム
いまいち、今自分の課題でalloyがここに使える、というイメージができてないんだよな