diff --git a/Tutorials/T04-A2Example/slides/T4.pdf b/Tutorials/T04-A2Example/slides/T4.pdf index 947a660279b7a615a98d5038cb66246ca4eee6e9..506422a1c8e0669f7132842052f2ba37d78850ec 100644 Binary files a/Tutorials/T04-A2Example/slides/T4.pdf and b/Tutorials/T04-A2Example/slides/T4.pdf differ diff --git a/Tutorials/T04-A2Example/slides/T4.tex b/Tutorials/T04-A2Example/slides/T4.tex index 6094c23ff46f815c39a1cc31921b4d7b1a8dc11e..081582e0120998595774877c3d67ddcab8e98a05 100644 --- a/Tutorials/T04-A2Example/slides/T4.tex +++ b/Tutorials/T04-A2Example/slides/T4.tex @@ -130,8 +130,8 @@ McMaster University\\ } \frametitle{What is a MIS?} \begin{itemize} \item Module Interface Specification \item Specifices externally observable behaviour of a module - \item Not in language of implementation, but uses mathematical and application language - \item Internal implementations are not included in a MIS + \item Not in language of implementation, uses mathematical language + \item Implementation details are not included in the MIS \end{itemize} \end{frame} @@ -193,7 +193,7 @@ McMaster University\\ } Consider the following triangle: \begin{figure}[h] \centering - \includegraphics[width=0.5\textwidth]{triangle.png} +% \includegraphics[width=0.5\textwidth]{triangle.png} \end{figure} We are using the following inequality which is called inequality equation to know the possibility of having triangle with three points A, B and C: @@ -233,7 +233,7 @@ N/A \textbf{Syntax}\\ Exported Types: \newline -pointT = ? +PointT = ? \end{frame} @@ -248,13 +248,13 @@ pointT = ? \hline \textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\ \hline -init & real, real & pointT & ~\\ +new PointT & real, real & PointT & ~\\ \hline xcoord & ~ & real & ~\\ \hline ycoord & ~ & real & ~\\ \hline -dist & pointT & real & ~\\ +dist & PointT & real & ~\\ \hline \end{tabular} @@ -277,10 +277,7 @@ None ~\newline \textbf{Assumptions} -init() is called for each abstract object before any other access routine is called for that object - - - +None \end{frame} @@ -294,7 +291,7 @@ init() is called for each abstract object before any other access routine is cal \textbf{Access Routine Semantics}\\ -init($x, y$): +PointT($x, y$): \begin{itemize} \item transition: $xc, yc := x, y$ \item output: $out := \mathit{self}$ @@ -319,17 +316,11 @@ init($x, y$): \item exception: none \end{itemize} - - - \end{frame} - - % -------------------------------------------------- - \begin{frame}[fragile] \frametitle{MIS Interface} @@ -369,16 +360,6 @@ From the MIS we can deduce the interface of the code will look like: % -------------------------------------------------- - -% -% -% -% -% -% - -% -------------------------------------------------- - \subsection{TriangleADT Module } \begin{frame} \frametitle{TriangleADT } @@ -406,13 +387,13 @@ TriangleADT = ?\\ \tabcolsep=0.09cm \begin{tabular}{| l | l | l | l |} \hline -\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\ +\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Except.}\\ %\hline %init & \multirow{2}{*}{Note 1} & Triangle & \\ \cline{1-3} \hline -init & pointT,pointT,pointT&TriangleADT & ~\\ +new TriangleT & PointT, PointT, PointT&TriangleADT & ~\\ \hline -sides & & &~\\ +sides & & seq[3] of real &~\\ \hline inequality\char`_theorem & ~ & boolean & LINE~\\ \hline @@ -432,97 +413,82 @@ area\char`_of\char`_triangle & & real & LINE ~\\ State Variables: -$p1$: pointT\\ -$p2$: pointT\\ -$p3$: pointT\\ -$AB$: real\\ -$AC$ : real\\ -$BC$ : real\\ +$p1$: PointT\\ +$p2$: PointT\\ +$p3$: PointT\\ + ~\newline \textbf{State Invariant} None ~\newline \textbf{Assumptions} -init() is called for each abstract object before any other access routine is called for that object - - - +None \end{frame} - % -------------------------------------------------- \begin{frame} - \textbf{Access Routine Semantics}\\ -init($p1, p2, p3$): +new TriangleT($a, b, c$): \begin{itemize} -\item transition: $a, b, c := p1, p2, p3$ +\item transition: $p1, p2, p3 := a, b, c$ \item output: $out := \mathit{self}$ \item exception: none \end{itemize} \noindent sides(): \begin{itemize} -\item transition: $AB, AC, BC := pointT.dist(self.a,self.b),$ -\\ $pointT.dist(slef.a,self.c), pointT.dist(self.b,self.c)$ -\item output: $out := \mathit{self}$ +\item output: $out := [p1.dist(p2), p1.dist(p3), p2.dist(p3)]$ \item exception: none \end{itemize} \end {frame} - - +% -------------------------------------------------- \begin {frame} -\noindent inequality theorem(): +\noindent inequality\_theorem(): \begin{itemize} -\item output: $$out := \mathrm {(self.AB +self.AC > self.BC\quad and \quad self.AB+self.BC }$$ - $$ \mathrm {> self.AC\quad and\quad self.AC+self.BC >self.AB)}$$ +\item output: +$out := ((self.sides[0] + self.slide[1]) > self.sides[2]$ + $\wedge (self.sides[1] + self.slide[2]) > self.sides[0]$ +$\wedge (self.sides[0] + self.slide[2]) > self.sides[1]$) \item exception: -\\ ex := ((self.a.xcoord()==self.b.xcoord() ==self.c.xcoord() or -\\ self.a.ycoord()==self.b.ycoord() ==self.c.ycoord()) $\Rightarrow \mbox{LINE})$ +\\ ex := ((p1.xcoord()==p2.xcoord() ==p3.xcoord() $\vee$ +\\ p1.ycoord()==p2.ycoord() ==p3.ycoord()) $\Rightarrow \mbox{LINE})$ \end{itemize} - - \end{frame} - % -------------------------------------------------- \begin{frame} -\noindent perimeter of triangle($ $): +\noindent perimeter\_of\_triangle($ $): \begin{itemize} -\item output: $$out := \mathrm{self.AB+self.AC+self.BC}$$ +\item output: $$out := self.sides[0]+self.sides[1]+self.sides[2]$$ \item exception: -\\ ex := ((self.a.xcoord()==self.b.xcoord() ==self.c.xcoord() or -\\ self.a.ycoord()==self.b.ycoord() ==self.c.ycoord()) $\Rightarrow \mbox{LINE})$ +\\ ex := ((p1.xcoord()==p2.xcoord() ==p3.xcoord() $\vee$ +\\ p1.ycoord()==p2.ycoord() ==p3.ycoord()) $\Rightarrow \mbox{LINE})$ \end{itemize} \noindent area of triangle($ $): \begin{itemize} -\item output : $$out :=\mathit {\sqrt[2]{P/2(P/2-self.AB)(P/2-self.AC)(P/2-self.BC)}}$$ +\item output : $out :=$ +${\sqrt[2]{P/2(P/2-self.sides[0])(P/2-self.sides[1])(P/2-self.sides[2])}}$ \item exception: -\\ ex := ((self.a.xcoord()==self.b.xcoord() ==self.c.xcoord() or -\\ self.a.ycoord()==self.b.ycoord() ==self.c.ycoord()) $\Rightarrow \mbox{LINE})$ +\\ ex := ((p1.xcoord()==p2.xcoord() ==p3.xcoord() $\vee$ +\\ p1.ycoord()==p2.ycoord() ==p3.ycoord()) $\Rightarrow \mbox{LINE})$ \end{itemize} -\textbf{Local Constants}\\ -P := self.AB+self.AC+self.BC - - +\textbf{Local Function}\\ +P := perimeter\_of\_triangle( ) \end{frame} - - % -------------------------------------------------- - \begin{frame}[fragile] \frametitle{MIS Interface} @@ -548,7 +514,6 @@ From the MIS we can deduce the interface of the code will look like: \end{lstlisting} - \end{frame} % -------------------------------------------------- @@ -559,14 +524,10 @@ From the MIS we can deduce the interface of the code will look like: \textbf{See TriangleADT for implementation.}\\ \end{center} - \end{frame} % -------------------------------------------------- - - -% ----------------------------------------------------- \begin{frame} \frametitle{Implementation files} \begin{itemize} @@ -575,6 +536,4 @@ From the MIS we can deduce the interface of the code will look like: \end{frame} - - \end{document}