Assignment 1

The assignments for 2004 are all inter-related, and address the problem of specifying a computer system for a large multi-story car park, details of which will be developed in what follows. The problem will be addressed in several stages, with additional specification and refinement being required at each stage.

1. You are to specify the basic behaviour of a car park. Cars arrive and leave the park at random intervals, and the car park has a finite capacity.
   1. Define data structures (using B Sets) to represent the state of the car park, and write these in the form of an abstract machine specification called $CarPark1$. \begin{answer}{0pt} Define a global set $CARS$ which is a set of all possible cars that might use the car park. Define a variable $cars\_in\_park$ which is a subset of $CARS$ \begin{tabbing} \bSetTabs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% MACHINE % %\bbnl {\bf MACHINE} \bhsp\+{\em CarPark1\/} \-\label{CarPark1}\index{CarPark1} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SETS % \bbnl {\bf SETS} \bhsp{\em CARS\/}\label{CARS}\index{CARS} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% VARIABLES % \bbnl {\bf VARIABLES} \bhsp{\em cars\_in\_park\/}\label{cars_in_park}\index{cars_in_park} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INVARIANT % \bbnl {\bf INVARIANT} \bhsp{\em cars\_in\_park\/} $\subseteq$ {\em CARS\/} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INITIALISATION % \bbnl {\bf INITIALISATION} \bhsp{\em cars\_in\_park\/} $:=$ $\emptyset$ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% END % \bbnl {\bf END} \end{tabbing} \end{answer}
   2. Add the operations $arrive(car)$ and $depart(car)$ to your specification. \ans %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% CarPark1.mch.tex % \bsetindent \begin{tabbing} \bSetTabs % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% MACHINE % %\bbnl {\bf MACHINE} \bhsp\+{\em CarPark1\/} \-\label{CarPark1}\index{CarPark1} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SETS % \bbnl {\bf SETS} \bhsp{\em CARS\/}\label{CARS}\index{CARS} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% VARIABLES % \bbnl {\bf VARIABLES} \bhsp{\em cars\_in\_park\/}\label{cars_in_park}\index{cars_in_park} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INVARIANT % \bbnl {\bf INVARIANT} \bhsp{\em cars\_in\_park\/} $\subseteq$ {\em CARS\/} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INITIALISATION % \bbnl {\bf INITIALISATION} \bhsp{\em cars\_in\_park\/} $:=$ $\emptyset$ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OPERATIONS % \bnl\bnl {\bf OPERATIONS} \+ \bbnl % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OPERATION arrive % {\bf { arrive}} ( {\em car\/} ) \bhsp $\defs$ \+ \bnl \bOpnWord{PRE} \+{\em car\/} $\in$ {\em CARS\/} \-\bnl \bOpnWord{THEN} \+{\em cars\_in\_park\/} $:=$ {\em cars\_in\_park\/} $\cup$ \{ \+{\em car\/} \- \} \-\bnl \bOpnWord{END} \- \bOperationSemiColon \bbnl % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OPERATION depart % {\bf { depart}} ( {\em car\/} ) \bhsp $\defs$ \+ \bnl \bOpnWord{PRE} \+{\em car\/} $\in$ {\em cars\_in\_park\/} \-\bnl \bOpnWord{THEN} \+{\em cars\_in\_park\/} $:=$ {\em cars\_in\_park\/} $-$ \{ \+{\em car\/} \- \} \-\bnl \bOpnWord{END} \-\- \bbnl % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% END % \bbnl {\bf END} \end{tabbing} \bresetindent
   Make sure you specify appropriate constraints and invariants in your specification.
2. A sophisticated monitoring system registers each car as it arrives and departs, and records the car registration plate in a manner similar to that used on the City Link tollways in Melbourne. The time and date of arrival and departure are also recorded for each car.
   1. Define a data structure for car registrations. What is the difference between a car registration and the car itself (as you defined in question 1)? Is this difference important to the specification process? Why (not)? \ans This is a trick question. You don't actually need a separate data structure to represent car registrations, since the element of the set $CARS$ defines the car perfectly adequately. It would only be if you needed to output a registration number for the car (which is a possible later refinement) that you need such a structure.
   2. Define a data structure for the arrival and departure times of a given car. \ans One perfectly reasonable scheme would be to use the same mechanism as is used to define time in Unix systems: seconds since 1 Jan 1970. For 32 bit signed numbers, this is appropriate until 19 Jan 2038 ($2^{31} \approx 2.1 \times 10^{9}$, or approximately 68.05 years since 1 Jan 1970). Hence the set $\nat$ suffices. We will define the synonym $TIME$ for this use of the natural numbers. Or you could use seconds since 1 Jan 2000 or any other (past) origin. If you use a data structure to represent days, hours, minutes, etc., you make life complicated for yourself when you come to manipulate them. Remember Occam's Razor: Always look for the simplest possible model! (Also known as the KISS or "Keep It Simple, Stupid!" principle :-)
   3. Define variables to model the arrival and departure times of a given car. \ans The best way to represent this is as a function, where the argument is the car, and the result is the time. We need two such functions, one for arrival and one for departure: $$arrival : CARS \pfun TIME$$ $$departure : CARS \pfun TIME$$ These are partial functions, since not all cars are in the car park. \item Add these data structures to your abstract machine $CarPark1$ to make $CarPark2$. How do the $arrive$ and $depart$ operations change? \ans %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% CarPark2.mch.tex % \bsetindent \begin{tabbing} \bSetTabs % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% MACHINE % %\bbnl {\bf MACHINE} \bhsp\+{\em CarPark2\/} \-\label{CarPark2}\index{CarPark2} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SETS % \bbnl {\bf SETS} \bhsp{\em CARS\/}\label{CARS}\index{CARS} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% CONSTANTS % \bbnl {\bf CONSTANTS} \bhsp{\em TIME\/}\label{TIME}\index{TIME} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PROPERTIES % \bbnl {\bf PROPERTIES} \bhsp{\em TIME\/} $=$ $\nat$ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% VARIABLES % \bbnl {\bf VARIABLES} \bhsp{\em cars\_in\_park\/}\label{cars_in_park}\index{cars_in_park} , {\em arrival\/}\label{arrival}\index{arrival} , {\em departure\/}\label{departure}\index{departure} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INVARIANT % \bbnl {\bf INVARIANT} \bhsp{\em cars\_in\_park\/} $\subseteq$ {\em CARS\/} $\wedge$ \bnl {\em arrival\/} $\in$ {\em CARS\/} $\pfun$ {\em TIME\/} $\wedge$ \bnl {\em departure\/} $\in$ {\em CARS\/} $\pfun$ {\em TIME\/} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INITIALISATION % \bbnl {\bf INITIALISATION} \bhsp{\em cars\_in\_park\/} $:=$ $\emptyset$ \bparallel \bnl {\em arrival\/} $:=$ $\emptyset$ \bparallel \bnl {\em departure\/} $:=$ $\emptyset$ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OPERATIONS % \bnl\bnl {\bf OPERATIONS} \+ \bbnl % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OPERATION arrive % {\bf { arrive}} ( {\em car\/} , {\em time\/} ) \bhsp $\defs$ \+ \bnl \bOpnWord{PRE} \+{\em car\/} $\in$ {\em CARS\/} $\wedge$ {\em time\/} $\in$ {\em TIME\/} \-\bnl \bOpnWord{THEN} \+\bnl {\em cars\_in\_park\/} $:=$ {\em cars\_in\_park\/} $\cup$ \{ \+{\em car\/} \- \} \bparallel \bnl {\em arrival\/} $:=$ {\em arrival\/} $<\kern-.65em\raisebox{.275ex}{$\scriptscriptstyle +$}\;$ \{ \+{\em car\/} $\mapsto$ {\em time\/} \- \} \-\bnl \bOpnWord{END} \- \bOperationSemiColon \bbnl % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OPERATION depart % {\bf { depart}} ( {\em car\/} , {\em time\/} ) \bhsp $\defs$ \+ \bnl \bOpnWord{PRE} \+{\em car\/} $\in$ {\em cars\_in\_park\/} $\wedge$ {\em time\/} $\in$ {\em TIME\/} $\wedge$ {\em time\/} $>$ {\em arrival\/} ( {\em car\/} ) \-\bnl \bOpnWord{THEN} \+\bnl {\em cars\_in\_park\/} $:=$ {\em cars\_in\_park\/} $-$ \{ \+{\em car\/} \- \} \bparallel \bnl {\em departure\/} $:=$ {\em departure\/} $<\kern-.65em\raisebox{.275ex}{$\scriptscriptstyle +$}\;$ \{ \+{\em car\/} $\mapsto$ {\em time\/} \- \} \-\bnl \bOpnWord{END} \-\- \bbnl % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% END % \bbnl {\bf END} \end{tabbing} \bresetindent