56858b1bb91d013

http://nhiro.org.s3.amazonaws.com/3/6/36e15f8f0e6160cd1111b00f8b7d48ca.jpg https://gyazo.com/36e15f8f0e6160cd1111b00f8b7d48ca

(OCR text)

BAlloy

14

SATソルバに入力するCNFを

人間に分かりやすい記述で生成するための言語

sig Object{

p cnf 57 78

-2 -1 -10 0

has: one Object

}

10 -14 0

-1 11 0

run {

-2 11 0

some Object

} for exactly 3 Object

12-11 0

57変数、78節

抽象によるソフトウェア設計

Alloy ではじめる形式手法

(not v2 or not v1 or not v10) and

(v10 or not v14) and ..

Daniel Jackson

Sitare Abstractions

抽象によるソフトウェア設計-Alloyではじめる形式手法

ONM