The Z Notation: A Reference Manual

BirthdayBookという仕様がある。
http://spivey.oriel.ox.ac.uk/~mike/zrm/

これをAlloyで書いてみた。

open util/relation

sig NAME {}
sig DATE {}

sig BirthdayBook {
  known: NAME,
  birthday : NAME -> lone DATE
} {
  known = dom[birthday]
}

pred AddBirthday [book,book':BirthdayBook, name:NAME, date:DATE] {
  name not in book.known
  book'.birthday = book.birthday + name -> date
}

pred FindBirthday [book:BirthdayBook, name:NAME, date:DATE] {
  name in book.known
  date = book.birthday[name]
}

pred Remind [book:BirthdayBook, today:DATE, cards : set NAME] {
  cards = { n: book.known | book.birthday[n] = today}
}

pred InitBirthdayBook [book:BirthdayBook] {
  book.known = none
}

enum REPORT {ok,already_known,not_known}
pred Success [result:REPORT] {
  result = ok
}

pred AlreadyKnown [book:BirthdayBook,name:NAME,result:REPORT] {
  name in book.known
  result = already_known
}

pred RAddBirthday [book,book':BirthdayBook,name:NAME,date:DATE,result:REPORT] {
  (name not in book.known and
    book'.birthday = book.birthday + name->date and
    result = ok) or
  (name in book.known and
    book'.birthday = book.birthday and
    result = already_known)
}

run {} for 3 NAME, 3 DATE, 3 BirthdayBook

書いて分かったけど、この仕様にはまずいところがあるよーな。
データモデルとして考えると、BirthdayBookがbirthdayを持つのでなく、
NAMEがbirthdayを持ったほうが良いんじゃないかと。