書籍「抽象によるソフトウェア設計 - Alloy ではじめる形式手法 -」を中心にして、Alloyによるモデル検査をみんなで勉強します。
ちなみにこのコミュニティのロゴは下記のAlloyのコードの5番目のインスタンスです。
sig Person{
liveIn: Place,
love: some Language
}
abstract sig Place {}
one sig Nagoya extends Place {}
abstract sig Language{}
one sig alloy, coq extends Language {}
pred PeopleInNagoyaLoveCoq {
all p:Person | p in liveIn.Nagoya & love.coq
}
run PeopleInNagoyaLoveCoq for 10