書籍「抽象によるソフトウェア設計 - Alloy ではじめる形式手法 -」を中心にして、Alloyによるモデル検査をみんなで勉強します。

ちなみにこのコミュニティのロゴは下記のAlloyのコードの５番目のインスタンスです。

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