Как спроектировать операцию поиска в нотации Z, при которой функция поиска требует хотя бы одной детали?

Question

Это моя схема Z для назначения DB.

|--AppointmentDB----------------
|attendees : P Person /** those involved in the appointment **/
|
|/** a new TYPE object to store attendees, schedule and purpose **/
|appointments : P APPOINTMENT
|hasAppointment : Person <-> APPOINTMENT
|schedule : APPOINTMENT -> DateTime
|purpose : APPOINTMENT -> Report 
|
|/** a forward relation compositions to relate attendees with purpose and schedule **/
|attendeePurpose : hasAppointment;purpose 
|attendeeSchedule : hasAppointment;schedule 
|-----------------------------
|attendees ⊆ dom(hasAppointment)
|attendees ⊆ dom(attendeePurpose)
|appointments ⊆ ran(hasAppointment)
|-----------------------------

Я хотел бы создать функцию поиска, которая находит встречу на основе имени attendees,

1. Я хочу, чтобы функция поиска возвращала все детали объекта встречи.

Как мне его оформить?

---

Вот мое взятие:

|--FindAppointment---------------------------------------------------
|ΞAppointmentDB
|attendees? : Person
|appointmentAttendees! : P Person
|appointmentPurpose! : Report
|appointmentSchedule! : DateTime
|-----------------------------
|/** if name of any attendees is given, then it must exist in appointments' domain
|respectively before this function can run**/
|attendees? ∈ dom(attendees)
|
|/** return the set of attendees of the same APPOINTMENT using attendees? as input **/
|appointmentAttendees! = hasAppointment~(|{attendees?}|)
|
|/** Get the image of both forward relational compositions according to set of 
|attendees?**/
|appointmentPurpose! =  attendeePurpose(|{attendees?}|)
|appointmentSchedule! = attendeeSchedule(|{attendees?}|)
|----------------------------------------------------------------------

Answer 1

Вы проверили свою спецификацию? Ваша декларация subject? : P Person говорится, что subject? это набор людей, но subject? : dom(attendees) подразумевает, что subject? это один человек.

• Если вы хотите, чтобы не было ни одного, ни одного человека, вы можете ввести тип данных, аналогичный монаде Maybe, в функциональных языках программирования (или нулевые значения в других языках программирования):

  MaybePerson ::= NoPerson | JustPerson <<Person>>
  

  Затем вы можете объявить вход как

  subject? : MaybePerson
  

  Тогда я бы предложил ограничить возможные решения для одного входа

  subject? : ran(JustPerson) => schedule! : schedule(|{ JustPerson~ subject? }|)
  

• Если subject? это набор людей, которых вы можете достичь с помощью:

  subject? /= {} => schedule! : schedule(|subject?|)
  

А затем просто сделайте то же самое для другого возможного ввода. Вы также можете добавить условие, что не обе записи должны быть NoPerson соответственно не оба входных набора должны быть пустыми.