Account. To log in means to associate a session with the
Accountof the user. This association is made in the relation
sessionAccount. To log out means to break that link, i.e. to remove the session/account pair from relation
sessionAccount. When logging in, it is customary that the user identifies herself. In this example we do this with a
UserIdis used to identify the user by a unique name. In this way, the (system generated) key of the user in the database is kept within the database.
Account, the system registers passwords. A
Passwordis a string of characters known to the user only. For this reason, the login service must not expose the password while the user is typing it.
SESSIONcorresponds with the notion of session as used in browsers. Ampersand links the session called
'_SESSION'to the current browser session, which results in the behaviour one would expect of a browser session.
BOX-es. The service is a box on the top level with two sub-boxes labeled
"_SESSION"[SESSION]as its box-term. What you must remember is that the every atom of the codomain of that term causes one contain (HTML:
<div>). In this example, the codomain of
"_SESSION"[SESSION]is just one atom, which is the session identifier. That is shown in the title of the outmost box in the browser.
"Login"and another labeled
"Logout". However, the outmost box was annotated with
Hstands for hidden. It means that empty subboxes will be hidden from the user. Now look at the box-terms of the
"Logout"subboxes. Which elements are in the codomain of the box-term of the
"Login"subbox? It says: "All sessions without an account associated with it". Since there is only one session (i.e. the browser-session) this comes down to "the current session, provided there is no account associated with it." So if nobody is logged in in the current browser session, the session atom is the only atom. Otherwise there is no atom and the
"Login"subbox is not shown. Similarly, which elements are there to make the the
"Logout"subbox appear? That box-term shows all sessions associated with an account. Which would be the account of the current session, provided someone is logged in.
"Login"subbox is shown when nobody is logged in and the
"Logout"subbox is shown when someone is logged in.