Interaction Formalization

GuestNr Updator [1] includes

@ get nextGuestNr() -> (nr: GuestNr) then

nr := nextGuestNr;

nextGuestNr := nextGuestNr+1;

end;

end;

Reservation Maker [1] includes

@ make reservation (g: GuestNr, n: Name, s: StreetNr, c: City,

a: ArrivalDate, d: NrDays, r: RoomNr) then

newGuest: Guest;

add Guest(newGuest);

add Guest(newGuest) has GuestNr(g);

add Guest(newGuest) with Name(n) lives on StreetNr(s) in City(c));

add Guest(newGuest) has reservation for Room(x) on

ArrivalDate(a) for NrDays(d) where Room(x) has RoomNr(r);

end;

end;

Previous slide

Next slide

Back to first slide

View graphic version