\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 2\\} \Large\textit{Total schemas with error checking} \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} [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 | OK $\\ \section{The State of the System} \begin{schema}{Computer} users, loggedIn:\power EMPLOYEE \where loggedIn \subseteq users \end{schema} \section{Initialisation} \begin{schema}{InitComputer} Computer' \where loggedIn' = \emptyset\\ users' = \emptyset \end{schema} \section{Change State Operations} \textit{Total} Operations defined here are:\\ i) Add User\\ ii) Remove User\\ iii) Log in\\ iv) Log out \pagebreak \subsection{Add User} Adds a new user. This is composed of two schema AddUser$_0$ and AddUserError. They will be combined into one using the schema disjunction operator ($\lor$). Why disjunction? Because either the AddUser$_0$ will be true resulting in a new user OR the AddUserError will be true resultinging in an error message being displayed.\\ AddUser$_0$ specifies that p? is a member of staff and should not be a member of users before the operation. It also specifies that after the completion of AddUser the set users' will include the new user, p? Any implementation should also not allow a change to the loggedIn set after the operation. \begin{schema}{AddUser_0} \Delta Computer\\ p? :EMPLOYEE \where p? \nin users\\ users' = users \cup \{p?\}\\ loggedIn' = loggedIn \end{schema} AddUserError completes the AddUser operation by specifying how to deal with any errors. Note the use of the Xi decoration which means there is no change to the state of the system by the AddUserError schema, it just declares a reply! output variable of type RESPONSE and specifies the system outputs "AlreadyAUser" when p? is indeed already a user. \begin{schema}{AddUserError} \Xi Computer\\ p?:EMPLOYEE\\ reply!: RESPONSE \where p? \in users\\ reply!=AlreadyAUser\\ \end{schema} Disjunction of AddUser$_0$ with AddUserError almost gives a complete AddUser schema but shouldn't the AddUser schema also output an all OK response when a user is successfully added? Why not. Disjunction of the two schemas and the addition of an OK response to the AddUser$_0$ schema is done below using a linear schema definition but alternatively you could have instead drawn another schema representing the OK Response, AddUser$_0$ and the AddUser together. The completed AddUser schema is:\\\\ $AddUser == \\(AddUser_0 \land [reply!:RESPONSE | reply!=OK]) \lor AddUserError$\\ \subsection{Remove User} Removes a user. The total remove User schema is described in a similar manner to the AddUser schema in the previous section. We define a RemoveUser$_0$ schema first. It specifies that p? is a member of staff and constrains p? to be a member of users before the operation. It also specifies that p? will be removed from users'. Any implementation should also ensure that p? is not logged in before the operation. Any implementation should also not allow a change to the loggedIn set after the operation. \begin{schema}{RemoveUser_0} \Delta Computer\\ p? :EMPLOYEE \where p? \in users\\ users' = users \setminus \{p?\}\\ p? \nin loggedIn\\ loggedIn' = loggedIn \end{schema} \\ The RemoveUserError specifies that p? should not be a user and a response "NotAUser" is specified as an output. Another error whould occur if p? is a user and logged in. We shouldn't remove a user while they are logged in so this schema specifies that where p? is a user and is logged in the reply "LoggedIn" should be output. Note the disjunction $\lor$ (or) that allows us to deal with both the case when p? is not a user and also when p? is a user. \begin{schema}{RemoveUserError} \Xi Computer\\ p?:EMPLOYEE\\ reply!: RESPONSE \where p? \nin users\\ reply!=NotAUser\\ \lor\\ p? \in users \land p?\in loggedIn \land response!=LoggedIn\\ \end{schema} \\ $RemoveUser == \\ (RemoveUser_0 \land [reply!:RESPONSE | reply!=OK]) \lor RemoveUserError$\\ \subsection{Log In} The total logIn specification is described in a similar manner to the RemoveUser schema in the previous section. We define a the LogIn$_0$ schema first. It specifies that p? is a member of staff and should be a member of users before the operation. It also specifies that p? should not be a member of loggedIn before the operation. It also specifies loggedIn' will include the new user, p? after the operation. \begin{schema}{LogIn_0} \Delta Computer\\ p? :EMPLOYEE \where p? \in users\\ p? \nin loggedIn\\ users' = users\\ loggedIn'=loggedIn \cup \{p?\}\\ \end{schema} An error should be flagged up if someone who is not a user tries to login or when a user is already loggedin. \begin{schema}{LogInError} \Xi Computer\\ p? :EMPLOYEE\\ reply!: RESPONSE \where (p? \nin users \land reply!=NotAUser)\\ \lor \\ (p? \in users \land p? \in 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? is a member of staff and should be a member of users before the operation. It also specifies that p? should be a member of loggedIn before the operation. It also specifies that p? will be removed from loggedIn' after the operation and that there will be no change in the set users' after the operation. \begin{schema}{LogOut_0} \Delta Computer\\ p? :EMPLOYEE \where p? \in users\\ p? \in loggedIn\\ users' = users\\ loggedIn'=loggedIn \setminus \{p?\}\\ \end{schema} The LogoutError specifies that a LogOut error will have occurred if a person who is not a user tries to logout or if a user who is not logged in tries to logout and the system will output a suitable logout error response. \begin{schema}{LogOutError} \Xi Computer\\ p? :EMPLOYEE\\ reply!: RESPONSE \where (p? \nin users \land reply!=NotAUser)\\ \lor \\ (p? \in users \land p? \nin loggedIn \land reply! = NotLoggedIn)\\ \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}