Updates to Intro to Verification slides

Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex

@@ -29,7 +29,7 @@
 \mode<presentation>{}
 
 \input{../def-beamer}
-\Drafttrue
+\Draftfalse
 
 \newcommand{\topicTitle}{29 Introduction to Verification (Ch.\ 6)}
 \ifDraft
@@ -73,19 +73,14 @@
 
 \begin{itemize}
 
-\item Investigating 9 academic integrity cases for A2
-
-\item A3 deadlines
+\item A3
 \begin{itemize}
-\item Part 2 - Code: due 11:59 pm Mar 20
-\item {Part 1 spec available in repo}
-\item \structure{Change of $<$ to $\leq$ in natural language and spec}
+\item Part 2 - Code: due 11:59 pm Mar 26
 \end{itemize}
 
 \item A4
 \bi
-\item Your own design and specification
-\item Due April 3 at 11:59 pm
+\item Due April 9 at 11:59 pm
 \ei
 
 \end{itemize}
@@ -94,12 +89,30 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\begin{frame}
+\frametitle{Advantages of Tables}
+
+\begin{itemize}
+
+\item Tabular expressions describe relations through pre and post conditions -
+  ideal for describing behaviour without sequences of operations
+\item They make it easy to ensure input domain coverage
+\item They are easy to read and understand (you need just a little practise to write them)
+\item Coding from tables results in extremely well structured code
+\item They facilitate identification of test cases
+\item Extremely good for real-time/embedded systems
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \begin{frame}
 \frametitle{A Table for pointInRegion(p)}
 
 \begin{itemize}
 
-\item Consider all of the cases
+\item Consider all of the cases for a rectangle
 \item Draw a picture
 \item Short form notation
 \begin{itemize}
@@ -110,47 +123,48 @@
 \item $llxw = \mathit{lower\_left}.\mbox{xcoord()} + \mathit{width}$
 \item $llyh = \mathit{lower\_left}.\mbox{ycoord()} + \mathit{height}$
 \item T = Constants.TOLERANCE
+\item $p1$.dist$(p2$) is the distance between p1 and p2
 \end{itemize}
 
 \end{itemize}
 
 \end{frame}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}[plain]
-\frametitle{Nine Cases}
+%\frametitle{A Table for Assignment 4, Part 2, pointInRegion(p)}
 
 \begin{tabular}{|p{2.cm}|p{2.8cm}|p{5.3cm}|}
 \hhline{~|~|-|}
 \multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
 \hhline{|-|-|-|}
-{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
+\uncover<2->{$px < llx$} & \uncover<3->{$py < lly$} & \uncover<4->{$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
 \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$lly \leq py \leq llyh$} & {$(llx - px) \leq \mbox{T}$}\\
+~ & \uncover<3->{$lly \leq py \leq llyh$} & \uncover<5->{$(llx - px) \leq \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
+~ & \uncover<3->{$py > llyh$} & \uncover<6->{$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
 \hhline{-|-|-|}
-{$llx \leq px \leq llxw$} & {$py < lly$} & {$(lly-py) \leq\mbox{T}$}\\
+\uncover<2->{$llx \leq px \leq llxw$} & \uncover<3->{$py < lly$} & \uncover<7->{$(lly-py) \leq\mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$lly \leq py \leq llyh$} & {$\mbox{True}$}\\
+~ & \uncover<3->{$lly \leq py \leq llyh$} & \uncover<8->{$\mbox{True}$}\\
 \hhline{|~|-|-|}
-~ & {$py > llyh$} & {$(py - llyh) \leq \mbox{T}$}\\
+~ & \uncover<3->{$py > llyh$} & \uncover<9->{$(py - llyh) \leq \mbox{T}$}\\
 \hhline{-|-|-|}
-{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
+\uncover<2->{$px > llxw$} & \uncover<3->{$py < lly$} & \uncover<10->{$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
 \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$lly \leq py \leq llyh$} & {$(px-llxw) \leq \mbox{T}$}\\
+~ & \uncover<3->{$lly \leq py \leq llyh$} & \uncover<10->{$(px-llxw) \leq \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw,llyh)) \leq \mbox{T}$}\\
+~ & \uncover<3->{$py > llyh$} & \uncover<10->{$p.\mbox{dist}(\mbox{PointT}(llxw,llyh)) \leq \mbox{T}$}\\
 \hhline{-|-|-|}
 
 \end{tabular}
 
 \end{frame}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
 \frametitle{Seven Cases}
@@ -159,29 +173,29 @@
 \hhline{~|~|-|}
 \multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
 \hhline{|-|-|-|}
-{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
+\uncover<1->{$px < llx$} & \uncover<1->{$py < lly$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
 \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$lly \leq py \leq llyh$} & {$(llx - px) \leq \mbox{T}$}\\
+~ & \uncover<1->{$lly \leq py \leq llyh$} & \uncover<1->{$(llx - px) \leq \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
+~ & \uncover<1->{$py > llyh$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
 \hhline{|-|-|-|}
-\multicolumn{2}{|l|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
+\multicolumn{2}{|l|}{\uncover<1->{$llx \leq px \leq llxw$}} & \uncover<2->{$(lly-\mbox{T}) \leq py \leq (llyh +
 \mbox{T})$}\\
 \hhline{|-|-|-|}
-{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
+\uncover<1->{$px > llxw$} & \uncover<1->{$py < lly$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
 \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$lly \leq py \leq llyh$} & {$(px-llxw) \leq \mbox{T}$}\\
+~ & \uncover<1->{$lly \leq py \leq llyh$} & \uncover<1->{$(px-llxw) \leq \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
+~ & \uncover<1->{$py > llyh$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
 \hhline{-|-|-|}
 
 \end{tabular}
 
 \end{frame}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
 \frametitle{Six Cases}
@@ -190,20 +204,20 @@
 \hhline{~|~|-|}
 \multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
 \hhline{|-|-|-|}
-{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
+\uncover<1->{$px < llx$} & \uncover<1->{$py < lly$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
 \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
+~ & \uncover<1->{$py > llyh$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
 \hhline{|-|-|-|}
-\multicolumn{2}{|l|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
+\multicolumn{2}{|l|}{\uncover<1->{$llx \leq px \leq llxw$}} & \uncover<1->{$(lly-\mbox{T}) \leq py \leq (llyh +
 \mbox{T})$}\\
 \hhline{|-|-|-|}
-{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
+\uncover<1->{$px > llxw$} & \uncover<1->{$py < lly$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
 \mbox{T}$}\\
 \hhline{|~|-|-|}
-~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
+~ & \uncover<1->{$py > llyh$} & \uncover<1->{$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
 \hhline{-|-|-|}
-\multicolumn{2}{|l|}{{$lly \leq py \leq llyh$}} & {$(llx-\mbox{T}) \leq px \leq (llxw +
+\multicolumn{2}{|l|}{\uncover<1->{$lly \leq py \leq llyh$}} & \uncover<2->{$(llx-\mbox{T}) \leq px \leq (llxw +
 \mbox{T})$}\\
 \hhline{|-|-|-|}
 
@@ -211,7 +225,7 @@
 
 \end{frame}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
 \frametitle{Three Cases}
@@ -220,14 +234,14 @@
 \hhline{~|~|-|}
 \multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
 \hhline{|-|-|-|}
-\multicolumn{2}{|p{5cm}|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
+\multicolumn{2}{|p{5cm}|}{\uncover<1->{$llx \leq px \leq llxw$}} & \uncover<1->{$(lly-\mbox{T}) \leq py \leq (llyh +
 \mbox{T})$}\\
 \hhline{|-|-|-|}
-\multicolumn{2}{|p{5cm}|}{{$lly \leq py \leq llyh$}} & {$(llx-\mbox{T}) \leq px \leq (llxw +
+\multicolumn{2}{|p{5cm}|}{\uncover<1->{$lly \leq py \leq llyh$}} & \uncover<1->{$(llx-\mbox{T}) \leq px \leq (llxw +
 \mbox{T})$}\\
 \hhline{|-|-|-|}
-\multicolumn{2}{|p{5cm}|}{{$\neg(llx \leq px \leq llxw) \wedge \neg(lly \leq py \leq llyh)$}} &
-{$\mbox{min}[p.\mbox{dist}(\mbox{PointT}(llx, lly)),$ $p.\mbox{dist}(\mbox{PointT}(llxw, lly)),$
+\multicolumn{2}{|p{5cm}|}{\uncover<1->{$\neg(llx \leq px \leq llxw) \wedge \neg(lly \leq py \leq llyh)$}} &
+\uncover<2->{$\mbox{min}[p.\mbox{dist}(\mbox{PointT}(llx, lly)),$ $p.\mbox{dist}(\mbox{PointT}(llxw, lly)),$
 $p.\mbox{dist}(\mbox{PointT}(llx, llyh)),$ 
 $p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) ] \leq \mbox{T}$}\\
 \hhline{|-|-|-|}
@@ -236,7 +250,7 @@ $p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) ] \leq \mbox{T}$}\\
 
 \end{frame}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
 \frametitle{Nine Cases, but 2D}