\documentclass[11pt,a4paper]{article} \usepackage{z-eves} \newcommand{\OPERATION}[1]{\textbf{#1:\ }} \newcommand{\ie}{\textit{i.e.}} \parindent 0pt \parskip 1.2ex plus 3pt \title{0657.424B Project: A Genealogy System} \author{Steve Reeves and PUT YOUR NAMES HERE} \begin{document} \maketitle \emph{Your task is to specify and test a genealogical (\ie\ family tree) database system. Do this by editing this file to extend the specification with the desired features. Submit the resulting .zed file, plus any other files that you think are necessary. For example, a *.jaza file that gives some positive and negative tests for each of the schemas that you define. Make sure that your final document reads like a specification that the software engineering group within the software house that is working on this project might have produced. (Remove this comment etc.)} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Introduction} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This document is a partial Z specification of a genealogical database system. Some of the basic operations are unspecified (denoted by sections marked by asterisks, and it is your job to define them) and some extensions to the existing system are required, and providing them will be your main task. \textbf{Document History:} \begin{description} \item[10th-12th September 2001:] Initial partial system typed by S. Reeves. Type checks and domain checks done using Z/EVES. \item[13th September 2001:] Released to 424 students so that they can specify the missing operations and the required extensions. \end{description} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Basic Definitions} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We assume the following basic set, without specifying details of what information constitutes a person. \begin{zed} [PERSON] \end{zed} We also define a set to record the gender of an individual. \begin{zed} GENDER ::= male | female \end{zed} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Basic Genealogical System} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The state of the system is given by: \begin{schema}{GDB} parent : PERSON \rel PERSON \\ sex: PERSON \pfun GENDER \where \dom parent \subseteq \dom sex \\ \ran parent \subseteq \dom sex \\ \forall p : PERSON @ p \mapsto p \notin parent \plus \\ \forall p, r, q : PERSON @ \{p \mapsto q, p \mapsto r \} \subseteq parent \land \\ \t8 q \neq r \implies sex~q \neq sex~r \end{schema} $parent$ models the parent-child relationship: $x \mapsto y \in parent$ means that $y$ is $x$'s parent. The sex of all people in the database is modelled by the function $sex$, and $\dom sex$ is all the people in the database. $sex~ p$ is the sex of person $p$. The first two predicates in the schema mean that $parent$ only holds information about people in the database. The third predicate means that no one is their own ancestor. This is done by first taking the transitive closure of $parent$, \ie\ $parent \plus$, and then saying that someone being their own parent, \ie\ $p \mapsto p$, is not in the closure. The fourth predicate says that any one one person has a maximum of two parents (the first conjunct) and if they have two parents (we're restricting ourselves to biological parents here, clearly) then they must be of opposite sexes. This schema gives rise to a domain check that is hard to do in Z/EVES, though informally it is clearly true. The check requires that $q$ and $r$ are in the range of $sex$. Since $q$ and $r$ are in the range of $parent$ by assumption, and since the range of $parent$ is a subset of the range of $sex$ (by the second state predicate) it follows that $q$ and $r$ are in the range of $sex$, as required. The initial state simply says that the database is empty: \begin{schema}{InitGDB} GDB \where sex = \emptyset \\ parent = \emptyset \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Operations on the database} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The required operations for the system should allow a user to add a person, remove a person, add or remove a relationship, change the name of a person and change the sex of a person. First, to add a person (who must not already be in the database): \begin{schema}{AddPerson} \Delta GDB \\ name? : PERSON \\ form? : GENDER \where name? \notin \dom sex \\ sex' = sex \cup \{name? \mapsto form?\} \\ parent' = parent \end{schema} Next, to remove a person from the database: *****To be added****** Next, to add a relationship to the database: \begin{schema}{AddRel} \Delta GDB \\ off?, par? : PERSON \where \{off?, par?\} \subseteq \dom sex \\ off? \mapsto par? \notin parent \\ par? \mapsto off? \notin parent \\ \# (\{off?\} \dres parent) \leq 1 \\ \forall x : PERSON @ off? \mapsto x \in parent \implies sex~x \neq sex~ par? \\ parent' = parent \cup \{off? \mapsto par? \} \\ sex' = sex \end{schema} Here the preconditions require that: the offspring and parent are already in the database (the first predicate); they must not already be related (the second and third predicates); there must not be more that one parent already in the database for the offspring (the fourth predicate); if there is already a parent then their sex must not be the same as the new parent (the fifth predicate). If all these are satisfied the operation with add the approriate maplet to the $parent$, and leave $sex$ unchanged. This also has a domain check that is hard in Z/EVES but clearly true. In the fifth predicate we have to show that $par?$ is in the domain of $sex$, which is easy to see from the first predicate. We also have to show that $x$ is in the domain of $sex$, which follows since it is in the domain of $parent$ by assumption, and so in the domain of $sex$ by the state invariant. Next, to remove a relationship from the database: *****To be added****** %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Extensions to the database operations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Having put in place the basic operations for adding and removing information, we now present specifications for more particular operations. ******** These operations are currently given by their requirements. The group has to work on these so as to specify them as required. $ChangeName$: On the assumption that the set $PERSON$ contains people's names (and therefore assuming that all names are unique), this operation, given an old name and a new name, changes the name of the person with the old name to a person with the new name, leaving all other information unchanged. $ChangeSex$: Given the name of a person, this operation changes their sex. This is in fact quite hard to specify, since to maintain the condition that any two parents of a person have opposite sex, if a person who is a parent changes their sex, then the other parent must too, as must anyone else who has had children with either of these two people, and so on. $QueryDB$: This operation, given a person and a type of query (\ie\ parents, grandparents, grandchildren, descendants, siblings, aunts) will return the set of all people in the database that have the given relationship with the given named person. More specifically, the operation should allow us to get the (sets of) people who are: \begin{itemize} \item The parents of person $x?$; \item The grandparents of person $x?$; \item The grandchildren of person $x?$; \item The descendants of person $x?$; \item The siblings of person $x?$; \item The aunts of person $x?$. \end{itemize} $NoRels$: This operation returns the set of people in the database who have no relations in the database. $NoSibs$: This operation reurns the set of all people in the database who have no siblings in the database. $NumGens$: This operation, given a person, outputs the number of generations through which the person can trace their family history in the database. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Validation and Testing} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% This section describes how this specification has been validated. \emph{This can/should include: type checking using Z/EVES, proving the domain checks of Z/EVES (or, as I have in a couple of places, giving informal proofs if the Z/EVES ones are too hard), testing the new operations with positive and negative examples, formal inspection meetings, notes of unresolved issues, etc.} \end{document} % \begin{axdef} % LA, TXS, WSH : CITY % \end{axdef} % % \begin{axdef} % sep10 : DATE \\ % tenam, onepm : TIME % \end{axdef} % % \begin{zed} % test1 \defs InitBookings' \semi \\ % \t1 ScheduleFlight[from? := LA, to? := TXS, departdate? := sep10, % departtime? := onepm, duration? := 65, % seats? := (1 \upto 8) \cross \{A,F\}] % \end{zed} % % % % \LET f1 == (\mu FlightDetails | from="LA" \land to="TXS" \land \\ % \t3 departdate="10SEP" \land departtime="13:00" \land \\ % \t3 duration=65 \land seats=(1 \upto 8) \cross \{A,F\} \\ % \t3 @ \theta FlightDetails); % f2 == (\mu FlightDetails | from="NY" \land to="TXS" \land \\ % \t3 departdate="10SEP" \land departtime="9:00" \land \\ % \t3 duration=180 \land seats=(1 \upto 40) \cross \{A,C,D,F\} \\ % \t3 @ \theta FlightDetails); % f3 == (\mu FlightDetails | from="LA" \land to="WSH" \land \\ % \t3 departdate="10SEP" \land departtime="10:00" \land \\ % \t3 duration=80 \land seats=(1 \upto 15) \cross \{A,C,F\} \\ % \t3 @ \theta FlightDetails) @ \\ % scheduled = \{ ("AG10-10SEP", f1), ("AG2-10SEP", f2), ("AG55-10SEP", f3) \}\\