section prelude

section number_toolkit

section set_toolkit

section relation_toolkit parents set_toolkit

section function_toolkit parents relation_toolkit

section sequence_toolkit parents function_toolkit , number_toolkit

section standard_toolkit parents sequence_toolkit

section birthday parents standard_toolkit

[ NAME , DATE ]

BirthdayBook
known : ℙ NAME
birthday : NAME ⇸ DATE
known = dom birthday

AddBirthday
Δ BirthdayBook
name? : NAME
date? : DATE
name? ∉ known
birthday′ = birthday ∪ { name? ↦ date? }

Now we can put some informal text in the middle.

FindBirthday
Ξ BirthdayBook
name? : NAME
date! : DATE
name? ∈ known
date! = birthday ( name? )

Remind
Ξ BirthdayBook
today? : DATE
cards! : ℙ NAME
cards! = { n : known | birthday ( n ) = today? }

InitBirthdayBook
BirthdayBook′
known′ = { }

REPORT ::= ok | already_known | not_known

Success
result! : REPORT
result! = ok

AlreadyKnown
Ξ BirthdayBook
name? : NAME
result! : REPORT
name? ∈ known
result! = already_known

RAddBirthday == ( AddBirthday ∧ Success ) ∨ AlreadyKnown

NotKnown
Ξ BirthdayBook
name? : NAME
result! : REPORT
name? ∉ known
result! = not_known

RFindBirthday == ( FindBirthday ∧ Success ) ∨ NotKnown

RRemind == Remind ∧ Success