Sample solution for A4.

Assignments/A4/A4Soln/A4_soln.tex

+\documentclass[12pt,fleqn]{article}
+
+\usepackage{graphicx}
+\usepackage{paralist}
+\usepackage{amsfonts}
+\usepackage{amsmath}
+\usepackage{amssymb}
+
+
+\oddsidemargin 0mm
+\evensidemargin 0mm
+\textwidth 160mm
+\textheight 200mm
+\renewcommand\baselinestretch{1.0}
+
+\pagestyle {plain}
+\pagenumbering{arabic}
+
+\newcounter{stepnum}
+
+\title{Assignment 2}
+\author{COMP SCI 2ME3 and SFWR ENG 2AA4\\\\Rober Boshra}
+
+\begin {document}
+
+\maketitle
+
+Specifications of battleship are split across three modules: ShipADT, BoardADT, and GameModule. GameModule provides basic access to starting a game, making a move, and checking whether the game is over. BoardADT contains the BoardT type, specifying a single board pertaining to one player and including both ship placements and hits/misses. BoardT was designed to have a sequence of ShipTs and a sequence of already hit gridcells; this is opposed to a complete two-dimensional grid. Each ship in the game is represented as an instance of ShipT with its predefined size and position on the board. A ShipT also tracks how many of its parts have been hit; however, there is no explicit tracking of which part is hit, as that is already covered by BoardT's list of hit cells.
+
+\section* {ShipADT Module}
+
+\subsection* {Template Module}
+
+ShipADT
+
+\subsection* {Uses}
+
+N/A
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Constants}
+
+MISS\_ID = $-1$\\
+EMPTY\_ID = $0$\\
+HIT\_ID = $1$\\
+SHIPDESTROYED\_ID = $2$
+
+\subsubsection* {Exported Types}
+
+Gridcell = tuple of $(xpos: integer, ypos: integer)$\\
+ShipT = ?
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+new ShipT & integer, integer, integer, boolean & ShipT & SHIPERROR\\
+\hline
+hit & ~ & integer & ~\\
+\hline
+span & ~ & sequence of Gridcell & ~\\
+\hline
+posx & ~ & integer & ~\\
+\hline
+posy & ~ & integer & ~\\
+\hline
+size & ~ & integer & ~\\
+\hline
+hor & ~ & boolean & ~\\
+\hline 
+partsdestroyed & ~ & integer & ~\\
+\hline 
+
+\end{tabular}
+
+\subsection* {Semantics}
+
+\subsubsection* {State Variables}
+
+$x$: integer //X-position of leftmost part of the ship\\
+$y$: integer //Y-position of the topmost part of the ship\\
+$s$: integer //Size of the ship\\
+$h$: boolean //True if the ship is placed horizontally, false otherwise\\
+$d$: integer //Number of ship parts hit 
+
+\subsubsection* {State Invariant}
+None
+
+\subsubsection* {Assumptions}
+None
+
+\subsubsection* {Access Routine Semantics}
+
+\noindent new ShipT ($\mathit{xin},\mathit{yin},\mathit{s},  \mathit{hin}$):
+\begin{itemize}
+\item transition: $x, y, s, h, d := \mathit{xin},\mathit{yin},\mathit{s}, \mathit{i}, \mathit{hin}, 0$
+\item output: $out := \mathit{self}$
+\item exception: $exc := (s < 1 \lor posx < 0 \lor posy < 0 \Rightarrow SHIPERROR)$
+\end{itemize}
+
+\noindent span ()
+\begin{itemize}
+\item output: 
+	\begin{gather*}
+		out := || (\forall xb, yb: \mathbb{N} | (yb = y \land xb \in [x..
+	x+s] \land h)\\ \lor (xb = x \land 
+	yb \in [y..y+s] \land \neg h): < \langle xb,yb \rangle > )
+	\end{gather*}
+\end{itemize}
+
+\noindent hit ()
+\begin{itemize}
+\item transition: $d := d + 1$
+\item output: $out := (d = s \Rightarrow \mbox{SHIPDESTROYED\_ID} | d < s  \Rightarrow \mbox{HIT\_ID})$
+\end{itemize}
+
+\noindent posx ():
+\begin{itemize}
+\item output: $out := x$
+\end{itemize}
+
+
+\noindent posy ():
+\begin{itemize}
+\item output: $out := y$
+\end{itemize}
+
+\noindent hor ():
+\begin{itemize}
+\item output: $out := h$
+\end{itemize}
+
+\noindent size ():
+\begin{itemize}
+\item output: $out := s$
+\end{itemize}
+
+\noindent partsdestroyed ():
+\begin{itemize}
+\item output: $out := d$
+\end{itemize}
+
+\section* {BoardADT Module}
+
+\subsection* {Template Module}
+
+BoardADT
+
+\subsection* {Uses}
+
+ShipADT
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Constants}
+
+SIZE\_X = 11\\
+SIZE\_Y = 9\\
+SHIP\_SIZES = $<2,3,3,4,5>$
+
+\subsubsection* {Exported Types}
+
+BoardT = ?
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+new BoardT & sequence of ShipT & BoardT & SETUPERROR\\
+\hline
+hit & integer, integer & integer & HITERROR\\
+\hline
+checkCell & integer, integer & integer & LOCATIONERROR\\
+\hline
+lose & ~ & boolean & ~\\
+\hline 
+
+\end{tabular}
+
+\subsection* {Semantics}
+
+\subsubsection* {State Variables}
+
+$ss$: sequence of ShipT //All ships that are part of the board\\
+$hits$: set of Gridcell //Tracks all actions taken against this board
+
+\subsubsection* {State Invariant}
+None
+
+\subsubsection* {Assumptions}
+Ships are passed to the constructor in the same order, in terms of size/type, as in SHIP\_SIZES.
+
+\subsubsection* {Access Routine Semantics}
+
+\noindent new BoardT ($\mathit{ships}$):
+\begin{itemize}
+\item transition: $ss, hits := ships, \{\}$
+\item output: $out := \mathit{self}$
+\item exception: $exec := (\neg correctsetup(ships) \Rightarrow \mbox{SETUPERROR})$
+\end{itemize}
+
+\noindent hit ($\mathit{x, y}$)
+\begin{itemize}
+\item transition: $hits := hits || \{ \langle x, y \rangle \} $
+\item output: $out := (\exists s: ShipT | s \in ss \land \langle x, y \rangle \in s.span() \Rightarrow s.hit() | \nexists s: ShipT | s \in ss \land \langle x, y \rangle \in s.span() \Rightarrow -1)$
+\item exception: $exec := \langle x, y \rangle \in hits \lor x \notin [1..\mbox{SIZE\_X}] \lor y \notin [1..\mbox{SIZE\_Y}]\Rightarrow \mbox{HITERROR})$
+\end{itemize}
+
+\noindent checkCell ($\mathit{x, y}$)
+\begin{itemize}
+\item output: 
+\begin{gather*}
+out := (\exists s: ShipT | s \in ss \land \langle x, y \rangle \in s.span()\\ \land \langle x, y \rangle \in hits \Rightarrow \mbox{ShipADT.HIT\_ID} 
+| \langle x, y \rangle \notin hits  \Rightarrow \mbox{ShipADT.EMPTY\_ID} \\
+| \nexists s: ShipT | s \in ss \land \langle x, y \rangle \in s.span() 
+\land \langle x, y \rangle \in hits \Rightarrow \mbox{ShipADT.MISS\_ID})
+\end{gather*}
+\item exception: $exec := x \notin [1..\mbox{SIZE\_X}] \lor y \notin [1..\mbox{SIZE\_Y}]\Rightarrow \mbox{LOCATIONERROR})$
+\end{itemize}
+
+\noindent lose ()
+\begin{itemize}
+\item output: $out := (\forall s: ShipT | s \in ships \land s.size() = s.partsdestroyed())$
+\end{itemize}
+
+\subsubsection*{Local Functions}
+\noindent correctsetup: sequence of ShipT $\rightarrow$ boolean
+
+\noindent $\mbox{correctsetup}(ships) \equiv $
+\begin{gather*}
+(\forall i: \mathbb{N} | ships[i].size() = SHIP\_SIZES[i] \land i < |SHIP\_SIZES|)\\ \land (\forall xp, yp, s: \mathbb{N}, \mathbb{N}, ShipT | s \in ships \land  \langle xp, yp \rangle \in s.span() \land  xp \in [1..\mbox{SIZE\_X}] \\ \lor yp \in [1..\mbox{SIZE\_Y]}) \land (\nexists cell, s1, s2: Gridcell, ShipT, ShipT | s1 \in ships \land s2 \in ships \\ \land cell \in s1.span() \land cell \in s2.span \land s1 \neq s2)
+\end{gather*}
+
+\newpage
+
+\section* {Battleship Game Module}
+
+\subsection* {Module}
+
+GameModule
+
+\subsection* {Uses}
+
+BoardADT
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+Game\_init & BoardT, BoardT & ~ & ~\\
+\hline
+Game\_p2turn & ~ & boolean & ~\\
+\hline
+Game\_hit & integer, integer & integer & ~\\
+\hline
+Game\_won & ~ & integer & ~\\
+\hline
+Game\_view & integer, integer & integer & ~\\
+\hline
+
+
+\end{tabular}
+
+\subsection* {Semantics}
+
+\subsubsection* {State Variables}
+$p1$: BoardT //First player's board (2nd player attacks it)\\
+$p2$: BoardT //Second player's board\\
+$turn$: boolean //Set to true if it is the second player's turn, the first player's if false
+
+\subsubsection* {Assumptions}
+Game\_init is called before any other access program.\\
+Game\_won is called after every Game\_hit. Game ends if the output is not 0 (a player won)
+
+\subsubsection* {Access Routine Semantics}
+
+\noindent Game\_init($x, y$):
+\begin{itemize}
+\item transition: $p1, p2, turn:=x, y, false$
+\end{itemize}
+
+\noindent Game\_hit($x, y$):
+\begin{itemize}
+\item transition: $turn := \neg turn$
+\item output: $out := currenttargetboard().hit(x,y)$
+\end{itemize}
+
+\noindent Game\_p2turn():
+\begin{itemize}
+\item output: $out := turn$
+\end{itemize}
+
+\noindent Game\_won():
+\begin{itemize}
+\item output: $out := p1.lose() \Rightarrow 2 | p2.lose() \Rightarrow 1 | \neg (p1.lose \lor p2.lose) \Rightarrow 0$  
+\end{itemize}
+
+\noindent Game\_view(x,y):
+\begin{itemize}
+\item output: $out := currenttargetboard().checkCell(x, y)$
+\end{itemize}
+
+\subsubsection*{Local Functions}
+\noindent currenttargetboard: () $\rightarrow$ BoardT
+
+\noindent $\mbox{currenttargetboard}() \equiv (turn \Rightarrow p1) | (\neg turn \Rightarrow p2)$
+
+\end{document}