\documentclass[a4paper]{article} \usepackage{zed-csp} \begin{document} \begin{titlepage} \vspace*{\stretch{1.0}} \begin{center} \Huge\textbf{Z Specification Example}\\ \huge\textit{Computer System Version 3\\} \Large\textit{Extending schemas with relations} \end{center} \vspace*{\stretch{2.0}} \endtitlepage \end{titlepage} %Example X schema\\ %Here is a simple specification \section{Introduction} A computer system that has multiple domains: Admin, Purchase, Retail and Booking. It also has multiple departments: Estates, Sales, Management, Office. The following table defines which Department members can login to which Domain. \begin{center} \begin{tabular}{ c c c c c } & Admin & Purchase & Retail & Booking \\ Estates & x & x & & \\ Sales & & x & x & x \\ Management & x & x & x & x \\ Office & x & x & & \\ \end{tabular} \end{center} \section{Types and Globals} [EMPLOYEE] set of all uniquely identifiable employees\\ Later we will need to respond to certain errors so here we need to define a RESPONSE type that is a freetype - a set of defined elements that make up the type.\\ RESPONSE::== $LoggedIn \mid NotLoggedIn | NotAUser | AlreadyAUser |AlreadyInADepartment | NotInADepartment | CannotAccessDomain | OK $\\ We'll need to initialise some more free types for working with relations later so here we go. For section 5.3 and 5.4 we need responses:-\\ DOMAIN::==$ Admin \mid Purchase | Retail | Booking\\$ DEPARTMENT::==$ Estates \mid Sales | Management | Office$\\ The following relations describe the relationships between DEPARTMENT and DOMAIN. This relation defines which department can access which computer domains.\\ Axiomatic box declaration for global \begin{axdef} canAccess: DEPARTMENT \rel DOMAIN\\ \end{axdef} \pagebreak \section{The State of the System} \begin{schema}{Computer} users:\power EMPLOYEE\\ belongsTo: EMPLOYEE \rel DEPARTMENT\\ loggedIn: EMPLOYEE \rel DOMAIN \end{schema} \section{Initialisation} We'll initialise canAccess here but it should really be empty initially and then operations defined to add or remove maplets in accordance with the specification. \begin{schema}{InitComputer} Computer' \where loggedIn' = \emptyset\\ users' = \emptyset\\ belongsTo' = \emptyset\\ canAccess' =\{Estates\mapsto Admin, Estates\mapsto Purchase, \\Sales \mapsto Purchase, Sales \mapsto Retail, Sales \mapsto Booking,\\ Management \mapsto Admin, Management \mapsto Purchase,\\ Management \mapsto Retail, Management \mapsto Booking,\\Office \mapsto Admin, Office \mapsto Purchase\} \end{schema} \section{Change State Operations} \textit{Total} Operations defined here are:\\ i) Add User\\ ii) Remove User\\ iii)Join Department\\ iv)Leave Department\\ v) Log in\\ vi) Log out \pagebreak \subsection{Add User} Adds a new user. This is composed of two schema AddUser$_0$ and AddUserError. \begin{schema}{AddUser_0} \Delta Computer\\ p? :EMPLOYEE \where p? \nin users\\ users' = users \cup \{p?\}\\ loggedIn' = loggedIn\\ belongsTo'=belongsTo\\ \end{schema} AddUserError completes the AddUser operation by specifying how to deal with any errors. \begin{schema}{AddUserError} \Xi Computer\\ p?:EMPLOYEE\\ reply!: RESPONSE \where p? \in users\\ reply!=AlreadyAUser\\ \end{schema} Disjunction of the two schemas and the addition of an OK response to the AddUser$_0$ schema completes the AddUser schema:\\\\ $AddUser == \\(AddUser_0 \land [reply!:RESPONSE | reply!=OK]) \lor AddUserError$\\ \subsection{Remove User} Removes a user. p? must be a user, must not belong to a department or be logged in. No other state changes to occur. \begin{schema}{RemoveUser_0} \Delta Computer\\ p? :EMPLOYEE \where p? \in users\\ users' = users \setminus \{p?\}\\ p? \nin \dom loggedIn\\ p? \nin \dom belongsTo\\ loggedIn' = loggedIn\\ belongsTo' = belongsTo \end{schema} \\ \begin{schema}{RemoveUserError} \Xi Computer\\ p?:EMPLOYEE\\ reply!: RESPONSE \where p? \nin users \land reply!=NotAUser\\ \lor\\ p? \in users \land p? \in \dom belongsTo \land response!=AlreadyInADepartment\\ \lor\\ p? \in users \land p?\in loggedIn \land response!=LoggedIn\\ \end{schema} \\ $RemoveUser == \\ (RemoveUser_0 \land [reply!:RESPONSE | reply!=OK]) \lor RemoveUserError$\\ \subsection{Join Department} We define the JoinDept$_0$ schema first. It specifies that p? will join department d? but p? must already be a user and not logged in. p? cannot join a department if they are already a member of another department. We will use the belongsTo relation for this operation together with the use of dom and ran operators.\\ The relation belongsTo is really a function so we could use the overriding $\oplus$ operator to we-write a maplet. \begin{schema}{JoinDept_0} \Delta Computer\\ p?:EMPLOYEE\\ dep?:DEPARTMENT \where p? \in users\\ p? \nin \dom belongsTo\\ users' = users\\ belongsTo'= belongsTo \cup \{p?\mapsto dep?\}\\ \end{schema} \begin{schema}{JoinDeptError} \Xi Computer\\ p? :EMPLOYEE\\ dep?:DEPARTMENT\\ reply!: RESPONSE \where p? \nin users \land reply!=NotAUser\\ \lor \\ p? \in users \land p? \in dom belongsTo \land reply! = AlreadyInADep\\ \end{schema} Disjunction of (JoinDept$_0$ and an OK response) with JoinDeptError now gives a complete JoinDept schema:\\ JoinDept == $(JoinDept_0 \land [reply!:RESPONSE | reply!=OK]) \lor $ JoinDeptError\\ \subsection{Leave Department} We define the LeaveDept$_0$ schema first. It specifies that p? will leave department d? but p? must already be a user and not logged in. p? cannot leave a department if they arenot a member of a department. We will use the belongsTo relation for this operation together with the use of dom and ran operators.\\ The relation belongsTo is really a function so we could other function operators to remove a maplet instead. \begin{schema}{LeaveDept_0} \Delta Computer\\ p?:EMPLOYEE\\ dep?:DEPARTMENT \where p? \in users\\ p? \in \dom belongsTo\\ users' = users\\ belongsTo'= belongsTo \setminus\{p? \mapsto dep?\}\\ p? \nin \dom loggedIn\\ loggedIn'=loggedIn \end{schema} \begin{schema}{LeaveDeptError} \Xi Computer\\ p? :EMPLOYEE\\ dep?:DEPARTMENT\\ reply!: RESPONSE \where p? \nin users \land reply!=NotAUser\\ \lor \\ p? \in users \land p? \nin \dom belongsTo \land reply! = NotInADepartment\\ \lor \\ p? \in users \land p? \in \dom loggedIn \land response!=LoggedIn \end{schema} Disjunction of (LeaveDept$_0$ and an OK response) with LeaveDeptError now gives a complete LeaveDept schema:\\ LeaveDept == $(LeaveDept_0 \land [reply!:RESPONSE | reply!=OK]) \lor $ LeaveDeptError\\ \subsection{Log In} We define the LogIn$_0$ schema first. It specifies that p? should be a member of users and has joined a department before the operation. It also specifies that p? should not be loggedIn before the operation. We test this by checking whether the dom of LoggedIn contains p? It also specifies loggedIn' will include the new maplet p?$ \mapsto $ d? after the operation. \begin{schema}{LogIn_0} \Delta Computer\\ p?:EMPLOYEE\\ d?:DOMAIN \where p? \in users\\ p? \nin \dom loggedIn\\ \{p?\mapsto d?\} \in belongsTo \comp canAccess\\ users' = users\\ belongsTo'=belongsTo\\ loggedIn'=loggedIn \cup \{p?\mapsto d?\}\\ \end{schema} An error should be flagged up if someone who is not a user tries to login or when a user is already logged in. We also check whether p? has access rights to the computer domain, d? If not then login fails. \begin{schema}{LogInError} \Xi Computer\\ p? :EMPLOYEE\\ d?:DOMAIN\\ reply!: RESPONSE \where p? \nin users \land reply!=NotAUser\\ \lor \\ p? \in users \land \{p?\mapsto d?\} \nin belongsTo \comp canAccess \land reply!=CannotAccessDomain\\ \lor\\ p? \in users \land p? \in \dom loggedIn \land reply! = LoggedIn\\ \end{schema} Disjunction of (LogIn$_0$ and an OK response) with LogInError now gives a complete LogIn schema:\\ LogIn == $(LogIn_0 \land [reply!:RESPONSE | reply!=OK]) \lor $ LoginError\\ \pagebreak \subsection{Log Out} As before we will create the total LogOut schema by combining LogIn$_0$ and LoginError schemas using a schema disjunction. The basic log out specification is logOut$_0$. It specifies that p? should be a member of users and belong to a department before the operation. It also specifies that p? should be logged in before the operation. It also specifies that the \{p?$\mapsto$ d?\} maplet will be removed from the loggedIn' relation after the operation and that there will be no other change to the computer system's state after the operation. \begin{schema}{LogOut_0} \Delta Computer\\ p? :EMPLOYEE\\ d?: DOMAIN \where p? \in users\\ \{p?\mapsto d?\} \in loggedIn\\ p? \in \dom belongsTo\\ users' = users\\ belongsTo'=belongsTo\\ loggedIn'=loggedIn \setminus \{p?\mapsto d?\}\\ \end{schema} The LogoutError specifies that a Log out error has occurred if a person who is not a user tries to log out or if a user who is not logged in tries to log out or if a person who is not a member of a department tries to log out and the system outputs a suitable error response. \begin{schema}{LogOutError} \Xi Computer\\ p? :EMPLOYEE\\ d?: DOMAIN\\ reply!: RESPONSE \where p? \nin users \land reply!=NotAUser)\\ \lor\\ p? \in users \land \{p?\mapsto d?\} \nin loggedIn \land reply! = NotLoggedIn\\ \lor \\ p? \in users \land p? \nin \dom belongsTo \land reply! = NotInADepartment\\ \end{schema} Disjunction of (LogOut$_0$ and an OK response) with LogOutError now gives a complete LogOut schema:\\ LogOut == $(LogOut_0 \land [reply!:RESPONSE | reply!=OK]) \lor $ LogOutError\\ \end{document}