diff --git a/Lectures/L28_ParnasTables/ParnasTables.pdf b/Lectures/L28_ParnasTables/ParnasTables.pdf index 2153a1ee22602bd21dbfdd289d52507005e14167..b567152352e16e7a6da708cbfe2985f1e9179de7 100644 Binary files a/Lectures/L28_ParnasTables/ParnasTables.pdf and b/Lectures/L28_ParnasTables/ParnasTables.pdf differ diff --git a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf index d3082a3e752232cf8e7cff64fc3a7914ea10105a..27fa7f5622f63b9de0f54f5f94057d9c9d776743 100644 Binary files a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf and b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf differ diff --git a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex index f6b03926e9c443e9f86b6c95d1125199ae331f76..7a2427646d6871b56502887e0e18d3ff02bb1129 100755 --- a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex +++ b/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}