diff --git a/Lectures/L18_MazeTracingRobot/MazeTracingRobot.pdf b/Lectures/L18_MazeTracingRobot/MazeTracingRobot.pdf
index 3fcfc51856aa2e8251f22c233346a19264744840..b11a3972e9c835c6773767d274f8a050f45c523b 100644
Binary files a/Lectures/L18_MazeTracingRobot/MazeTracingRobot.pdf and b/Lectures/L18_MazeTracingRobot/MazeTracingRobot.pdf differ
diff --git a/Lectures/L18_MazeTracingRobot/MazeTracingRobot.tex b/Lectures/L18_MazeTracingRobot/MazeTracingRobot.tex
index 2ded1f0639201dec3963520c0bf236f8c5afe32a..7d437b4a55b3e408b51cf629b71089392e6f9367 100755
--- a/Lectures/L18_MazeTracingRobot/MazeTracingRobot.tex
+++ b/Lectures/L18_MazeTracingRobot/MazeTracingRobot.tex
@@ -1,73 +1,76 @@
-%\documentclass[13pt]{beamer} % some colour, looks good with logictheme style
-\documentclass[handout]{beamer} % for handout
-%\documentclass{beamer} % for slides using uncover
+%\documentclass[t,12pt,numbers,fleqn,handout]{beamer}
+\documentclass[t,12pt,numbers,fleqn]{beamer}
 
-\usepackage{logictheme}
-\usepackage{amsmath}
-\usepackage{bm}
-\usepackage{ulem}
-
-\usepackage{hhline}
-\usepackage{multirow}
-\usepackage{multicol}
-\usepackage{array}
+\usepackage{pgfpages} 
 \usepackage{hyperref}
+\hypersetup{colorlinks=true,
+    linkcolor=blue,
+    citecolor=blue,
+    filecolor=blue,
+    urlcolor=blue,
+    unicode=false}
+\urlstyle{same}
+
+\usepackage{booktabs}
+\usepackage{multirow}
 
-\usepackage{listings}
+\useoutertheme{split} %so the footline can be seen, without needing pgfpages
 
-\title[Maze Tracing Robot (slide \thepage)]{Maze Tracing Robot Example}
-%\subtitle{???}
-\author[Smith]{Dr.~Spencer Smith}
-\institute{Computing and Software Department, McMaster University}
-\date{\today}
-\pgfdeclareimage[height=0.5cm]{logo}{../McMasterLogo} %McMaster logo in one folder up
-\logo{\pgfuseimage{logo}}
+% \pgfpagesuselayout{resize to}[letterpaper,border
+% shrink=5mm,landscape] %if this is uncommented, the hyperref links do not work
 
-\setbeamercolor{alerted text}{fg=red!75!green!50!blue}
-%\setbeamerfont{alerted text}{series=\bfseries}
-\setbeamerfont{alerted text}{family=\rmfamily,series=\bfseries}
+\mode<presentation>{}
 
-%\setbeamertemplate{footline}{\insertpagenumber}  % only has the page number
+\input{../def-beamer}
 
-\newcounter{temp}
+\newcommand{\topic}{18 Maze Tracing Robot Example}
+
+\input{../titlepage}
 
 \begin{document}
 
-% ==================================================================================
-% Slide 1
-\maketitle
-% ==================================================================================
+\input{../footline}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
 \frametitle{Maze Tracing Robot Example}
 
 \begin{itemize}
 \item Administrative details
-\item Dr.\ v.\ Mohrenschildt's maze tracing robot (see WebCT document)
+\item Index set example
+\item Solar water heating tank example
+\item Dr.\ v.\ Mohrenschildt's maze tracing robot (see GitLab)
 \item MIS for maze\_storage
 \end{itemize}
 
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \begin{frame}
 \frametitle{Administrative Details}
 
 \begin{itemize}
 
-\item Assignment 3 deadlines
+\item Assignment 2
 \begin{itemize}
-\item Minor modifications to posted file
-\item Code due by midnight Feb 23
-\item E-mail your partner your code by  Feb 24
-\item Lab report due by the beginning of class Mar 2
-\item Will discuss Assignment 3 during tutorial, time for questions
+\item {Files due by 11:59 pm Feb 19}
+\item {File automatically sent to partners on Feb 20}
+\item Lab report due by 11:59 pm Feb 27
+\item {When returning an object, you can either create a new object or
+    return a reference}
+\item {Remember: Deque is an Abstract Object, not an ADT}
 \end{itemize}
+
 \item Midterm exam
 \begin{itemize}
-\item March 4 during tutorial time
-\item In T29/105, not our usual classroom
+\item March 1, 7:00 pm, TSH/120
+\item 90 minute duration
+\item Multiple choice - 30--40 questions?
+\item Open book (any paper)
 \end{itemize}
+
 \end{itemize}
 
 \end{frame}
@@ -75,170 +78,151 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-\frametitle{Modules with External Interaction}
+\frametitle{Index Set}
 
-\begin{itemize}
-\item In general, some modules may interact with the environment or other modules
-%\item The Display Point Masses Applet module does this
-\item Environment might include the keyboard, the screen, the file system, motors, sensors, etc.
-\item Sometimes the interaction is informally specified using prose (natural language)
-\item Can introduce an environment variable
-\begin{itemize}
-\item Name, type
-\item Interpretation
-\end{itemize}
-\item Environment variables include the screen, the state of a motor (on, direction of rotation, power level, etc.),
-the position of a robot
-
-\end{itemize}
+Write a function \texttt{indexSet(x, B)} that takes a value \texttt{x} and a
+list of values \texttt{B} and returns a list of indices where \texttt{B[i] =
+  x}.\\
+~\newline
+As a first step, how would you say this mathematically?
 
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-\frametitle{External Interaction Continued}
+\frametitle{Index Set}
 
-\begin{itemize}
-\item Some external interactions are hidden
-\begin{itemize}
-\item Present in the implementation, but not in the MIS
-\item An example might be OS memory allocation calls
-\end{itemize}
-\item External interaction described in the MIS
-\begin{itemize}
-\item Naming access programs of the other modules
-\item Specifying how the other module's state variables are changed
-\item The MIS should identify what external modules are used
-\end{itemize}
-\end{itemize}
+Write a function \texttt{indexSet(x, B)} that takes a value \texttt{x} and a
+list of values \texttt{B} and returns a list of indices where \texttt{B[i] =
+  x}.\\
+
+$$\mbox{indexSet}(x, B) \equiv \{i : \mathbb{N} | i \in [0 .. |B|-1] \wedge B_i =
+x : i\}$$
+
+How could you use \texttt{indexSet} to calculate \texttt{rank(x, A)}?
 
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}
-\frametitle{MIS for GUI Modules}
 
-\begin{itemize}
-\item Could introduce an environment variable
-\item window: sequence [RES\_H][RES\_V] of pixelT
-\begin{itemize}
-\item Where window[r][c] is the pixel located at row r and column c, with numbering zero-relative and beginning at the
-upper left corner
-\item Would still need to define pixelT
-\end{itemize}
-\item Could formally specify the environment variable transitions
-\item More often it is reasonable to specify the transition in prose
-\item In some cases the proposed GUI might be shown by rough sketches
-\end{itemize}
+\begin{frame}
+\frametitle{Anticipated Changes}
+
+\bi
+\item The specific hardware on which the software is to run
+\item The format of the initial input data
+\item The format of the input parameters
+\item The constraints on the input parameters
+\item The format of the output data
+\item The constraints on the output results
+\item How the governing ODEs are defined using the input parameters
+\item How the energy equations are defined using the input parameters
+\item How the overall control of the calculations is orchestrated
+\item The implementation of the sequence data structure
+\item The algorithm used for the ODE solver
+\item The implementation of plotting data
+\ei
 
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-\frametitle{Display Point Masses Module Syntax}
+\frametitle{Module Hierarchy by Secrets}
+\begin{table}[h!]
+\centering
+\begin{tabular}{p{0.3\textwidth} p{0.6\textwidth}}
+\toprule
+\textbf{Level 1} & \textbf{Level 2}\\
+\midrule
+
+{Hardware-Hiding Module} & ~ \\
+\midrule
+
+\multirow{6}{0.3\textwidth}{Behaviour-Hiding Module} & Input Format Module\\
+& Input Parameters Module\\
+& Output Format Module\\
+& Temperature ODEs Module\\
+& Energy Equations Module\\ 
+& Control Module\\
+\midrule
+
+\multirow{3}{0.3\textwidth}{Software Decision Module} & {Sequence Data Structure Module}\\
+& ODE Solver Module\\
+& Plotting Module\\
+\bottomrule
 
-\textbf{Exported Access Programs}\\
-~\newline
-\begin{tabular}{| l | l | l | l |}
-\hline
-\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exc.}\\
-\hline
-DisplayPointMassesApplet & ~ & DisplayPointMassesApplet & ~\\
-\hline
-paint & ~ & ~ & ~\\
-\hline
 \end{tabular}
-
+\caption{Module Hierarchy}
+\label{TblMH}
+\end{table}
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-\frametitle{Display Point Masses Module Semantics}
+\frametitle{Example Modules from SWHS}
 
-\textbf{Environment Variables}\\
-$\mathit{win}:$ 2D sequence of pixels displayed within a web-browser \\
+\textbf{Hardware Hiding Modules}
 
-\noindent DisplayPointMassesApplet():
-\begin{itemize}
-\item transition: The state of the abstract object ListPointMasses is modified as follows:\\
-ListPointMasses.init()\\
-ListPointMasses.add(0, PointMassT(20, 20, 10)\\
-ListPointMasses.add(1, PointMassT(120, 200, 20)\\
-...
-\end{itemize}
-
-\noindent paint():
-\begin{itemize}
-\item transition $win := $ Modify window so that the point masses in ListPointMasses 
-are plotted as circles.  The centre of each circles should be the corresponding x and y coordinates and the radius should
-be the mass of the point mass.
-\end{itemize}
+\begin{description}
+\item[Secrets:]The data structure and algorithm used to implement the virtual
+  hardware.
+\item[Services:]Serves as a virtual hardware used by the rest of the
+  system. This module provides the interface between the hardware and the
+  software. So, the system can use it to display outputs or to accept inputs.
+\item[Implemented By:] OS
+\end{description}
 
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \begin{frame}
-\frametitle{Assignment 3 Vector Module}
+\frametitle{Example Modules from SWHS}
 
-\textbf {Exported Access Programs}\\
-~\newline
-\begin{tabular}{| l | l | l | p{0.75in} |}
-\hline
-\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
-\hline
-new vectorT & real $\rightarrow$ real & vectorT & ~\\
-\hline
-getf & ~ & real $\rightarrow$ real & ~\\
-\hline
-eval & real, real, integer & sequence of real & deltaNeg, nstepsNeg\\
-\hline
-evalPrint & real, real, integer & ~ & deltaNeg, nstepsNeg\\
-\hline
-\end{tabular}
+\textbf{Input Verification Module}
+
+\begin{description}
+\item[Secrets:] The rules for the physical and software constraints.
+\item[Services:] Verifies that the input parameters comply with physical and
+  software constraints. Throws an error if a parameter violates a physical
+  constraint. Throws a warning if a parameter violates a software constraint.
+\item[Implemented By:] SWHS
+\end{description}
 
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-\frametitle{Vector Module Semantics}
+\frametitle{Example Modules from SWHS}
 
-\textbf{Environment Variables}\\
-$\mathit{screen}$ : two dimensional sequence of positions on the screen, which each position holding a character\\
-~\newline
-\textbf{State Variables}\\
-$f$: real $\rightarrow$ real\\
-~\newline
-\textbf{Access Routine Semantics}\\
-\noindent eval ($\mathit{startx}, \mathit{deltax}, \mathit{nsteps}$):
-\begin{itemize}
-\item output: $out := < f(\mathit{startx}), f(\mathit{startx} + \mathit{deltax}), f(\mathit{startx} + 2 \cdot \mathit{deltax}), ...
-, f(\mathit{startx} + \mathit{nsteps} \cdot \mathit{deltax})>$
-\item exception: $exc := ((\mathit{deltax} < 0) \Rightarrow  \mbox{deltaNeg} | (\mathit{nsteps} < 0) \Rightarrow
-\mbox{nstepsNeg})$
-\end{itemize}
+\textbf{ODE Solver Module}
+
+\begin{description}
+\item[Secrets:] The algorithm to solve a system of first order ODEs.
+\item[Services:] Provides solvers that take the governing equation, initial
+  conditions, and numerical parameters, and solve them.
+\item[Implemented By:] Matlab
+\end{description}
 
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{frame}
-\frametitle{Vector Module Semantics Continued}
+\begin{frame}[plain, fragile]
 
-\noindent evalPrint ($\mathit{startx}, \mathit{deltax}, \mathit{nsteps}$):
-\begin{itemize}
-\item transition: The state of $\mathit{screen}$ is modified so that the sequence returned by eval ($\mathit{startx}$,
-$\mathit{deltax}$, $\mathit{nsteps}$) is displayed.
-\item exception: $exc := ((\mathit{deltax} < 0) \Rightarrow  \mbox{deltaNeg} | (\mathit{nsteps} < 0) \Rightarrow
-\mbox{nstepsNeg})$
-\end{itemize}
+\frametitle{SWHS Uses Hierarchy}
+
+\begin{center}
+\includegraphics[scale=0.55]{UsesHierarchy.pdf}
+\end{center}
 
 \end{frame}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
 \frametitle{Dr.\ v.\ Mohrenschildt's Maze Tracing Robot Example}
@@ -254,7 +238,8 @@ $\mathit{deltax}$, $\mathit{nsteps}$) is displayed.
 \frametitle{Maze Tracing Robot Expected Changes}
 
 \begin{itemize}
-\item Changes to the geometry of the robot such that the mapping from a position to the robot inputs is different
+\item Changes to the geometry of the robot such that the mapping from a position
+  to the robot inputs is different
 \item Changes to the interface to the robot
 \item Changes to the format of the maze
 \item Changes to any constant values
@@ -306,20 +291,23 @@ $\mathit{deltax}$, $\mathit{nsteps}$) is displayed.
 \begin{itemize}
 \item \structure<1>{Module name:} control
 \begin{itemize}
-\item \structure<1>{Secret:} how the arm moves from position to position and how the buttons are checked
+\item \structure<1>{Secret:} how the arm moves from position to position and how
+  the buttons are checked
 \item \structure<1>{Service:} controls the movement of the arm
 \item \structure<1>{Module prefix:} cn\_
 \end{itemize}
 \item \structure<1>{Module name:} geometry
 \begin{itemize}
-\item \structure<1>{Secret:} how the calculations from cell coords to robot coords are performed
+\item \structure<1>{Secret:} how the calculations from cell coords to robot
+  coords are performed
 \item \structure<1>{Service:} handles geometric positioning of the arm
 \item \structure<1>{Module prefix:} gm\_
 \end{itemize}
 \item \structure<1>{Module name:} hardware
 \begin{itemize}
 \item \structure<1>{Secret:} how it interfaces with the robot
-\item \structure<1>{Service:} handles hardware aspects of arm (movement and button checking)
+\item \structure<1>{Service:} handles hardware aspects of arm (movement and
+  button checking)
 \item \structure<1>{Module prefix:} hw\_
 \end{itemize}
 \end{itemize}
@@ -332,8 +320,10 @@ $\mathit{deltax}$, $\mathit{nsteps}$) is displayed.
 \begin{itemize}
 \item \structure<1>{Module name:} types\_constants
 \begin{itemize}
-\item \structure<1>{Secret:} how the data structures are defined and constants defined
-\item \structure<1>{Service:} provides standard variable types and constants to modules
+\item \structure<1>{Secret:} how the data structures are defined and constants
+  defined
+\item \structure<1>{Service:} provides standard variable types and constants to
+  modules
 \end{itemize}
 \end{itemize}
 \end{frame}
@@ -410,8 +400,8 @@ cell = tuple of (x: integer, y: integer)
 % there could be one related to maximum size of the map
 ~\newline
 \textbf{Assumptions}\\
-~\newline
-ms\_get\_maze\_start and ms\_get\_maze\_end are not called until after the corresponding set routines have been called.
+~\newline ms\_get\_maze\_start and ms\_get\_maze\_end are not called until after
+the corresponding set routines have been called.
 
 \end{frame}
 
@@ -520,7 +510,6 @@ ms\_get\_maze\_start and ms\_get\_maze\_end are not called until after the corre
 \frametitle{Additional Specifications for Determining the Path}
 
 pathT = sequence of cell\\
-~\newline
 
 \noindent validPath : pathT $\rightarrow$ boolean
 \begin{itemize}
diff --git a/Lectures/L18_MazeTracingRobot/UsesHierarchy.pdf b/Lectures/L18_MazeTracingRobot/UsesHierarchy.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..a229222f5284ff31b7e96c88ae67d0c2a012bd50
Binary files /dev/null and b/Lectures/L18_MazeTracingRobot/UsesHierarchy.pdf differ
diff --git a/Lectures/L19_ModulesWithExternalInteraction/ExampleMaze.pdf b/Lectures/L19_ModulesWithExternalInteraction/ExampleMaze.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..02a84ef3d83cf7a1c0afaf83af288cc612dc63ae
Binary files /dev/null and b/Lectures/L19_ModulesWithExternalInteraction/ExampleMaze.pdf differ
diff --git a/Lectures/L19_ModulesWithExternalInteraction/MazeTracingRobot.pdf b/Lectures/L19_ModulesWithExternalInteraction/MazeTracingRobot.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..4a3f2923cac0dd7f9acc71fb5f1de80a127f0d6e
Binary files /dev/null and b/Lectures/L19_ModulesWithExternalInteraction/MazeTracingRobot.pdf differ
diff --git a/Lectures/L19_ModulesWithExternalInteraction/MazeTracingRobot.tex b/Lectures/L19_ModulesWithExternalInteraction/MazeTracingRobot.tex
new file mode 100755
index 0000000000000000000000000000000000000000..89113604e086c8158c0374e3d139d445e493ab81
--- /dev/null
+++ b/Lectures/L19_ModulesWithExternalInteraction/MazeTracingRobot.tex
@@ -0,0 +1,710 @@
+%\documentclass[t,12pt,numbers,fleqn,handout]{beamer}
+\documentclass[t,12pt,numbers,fleqn]{beamer}
+
+\usepackage{pgfpages} 
+\usepackage{hyperref}
+\hypersetup{colorlinks=true,
+    linkcolor=blue,
+    citecolor=blue,
+    filecolor=blue,
+    urlcolor=blue,
+    unicode=false}
+\urlstyle{same}
+
+\usepackage{booktabs}
+\usepackage{multirow}
+
+\useoutertheme{split} %so the footline can be seen, without needing pgfpages
+
+% \pgfpagesuselayout{resize to}[letterpaper,border
+% shrink=5mm,landscape] %if this is uncommented, the hyperref links do not work
+
+\mode<presentation>{}
+
+\input{../def-beamer}
+
+\newcommand{\topic}{18 Maze Tracing Robot Example}
+
+\input{../titlepage}
+
+\begin{document}
+
+\input{../footline}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Maze Tracing Robot Example}
+
+\begin{itemize}
+\item Administrative details
+\item Index set example
+\item Solar water heating tank example
+\item Modules with external interaction
+\item Dr.\ v.\ Mohrenschildt's maze tracing robot (see GitLab)
+\item MIS for maze\_storage
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}
+\frametitle{Administrative Details}
+
+\begin{itemize}
+
+\item Assignment 2
+\begin{itemize}
+\item {Files due by 11:59 pm Feb 19}
+\item {File automatically sent to partners on Feb 20}
+\item Lab report due by 11:59 pm Feb 27
+\item {When returning an object, you can either create a new object or
+    return a reference}
+\item {\texttt{totalArea} is just the sum of the area of all circles,
+    do not worry about overlap}
+\item {Removed POS exception from syntax}
+\item {Implementation does NOT have to look like the
+    spec}
+\end{itemize}
+
+\item Midterm exam
+\begin{itemize}
+\item March 1, 7:00 pm, TSH/120
+\item 90 minute duration
+\item Multiple choice - 30--40 questions?
+\item Open book (any paper)
+\end{itemize}
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Index Set}
+
+Write a function \texttt{indexSet(x, B)} that takes a value \texttt{x} and a
+list of values \texttt{B} and returns a list of indices where \texttt{B[i] =
+  x}.\\
+~\newline
+As a first step, how would you say this mathematically?
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Index Set}
+
+Write a function \texttt{indexSet(x, B)} that takes a value \texttt{x} and a
+list of values \texttt{B} and returns a list of indices where \texttt{B[i] =
+  x}.\\
+
+$$\mbox{indexSet}(x, B) \equiv \{i : \mathbb{N} | i \in [0 .. |B|-1] \wedge B_i =
+x : i\}$$
+
+How could you use \texttt{indexSet} to calculate \texttt{rank(x, A)}?
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Anticipated Changes}
+
+\bi
+\item The specific hardware on which the software is to run
+\item The format of the initial input data
+\item The format of the input parameters
+\item The constraints on the input parameters
+\item The format of the output data
+\item The constraints on the output results
+\item How the governing ODEs are defined using the input parameters
+\item How the energy equations are defined using the input parameters
+\item How the overall control of the calculations is orchestrated
+\item The implementation of the sequence data structure
+\item The algorithm used for the ODE solver
+\item The implementation of plotting data
+\ei
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Module Hierarchy by Secrets}
+\begin{table}[h!]
+\centering
+\begin{tabular}{p{0.3\textwidth} p{0.6\textwidth}}
+\toprule
+\textbf{Level 1} & \textbf{Level 2}\\
+\midrule
+
+{Hardware-Hiding Module} & ~ \\
+\midrule
+
+\multirow{6}{0.3\textwidth}{Behaviour-Hiding Module} & Input Format Module\\
+& Input Parameters Module\\
+& Output Format Module\\
+& Temperature ODEs Module\\
+& Energy Equations Module\\ 
+& Control Module\\
+\midrule
+
+\multirow{3}{0.3\textwidth}{Software Decision Module} & {Sequence Data Structure Module}\\
+& ODE Solver Module\\
+& Plotting Module\\
+\bottomrule
+
+\end{tabular}
+\caption{Module Hierarchy}
+\label{TblMH}
+\end{table}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Example Modules from SWHS}
+
+\textbf{Hardware Hiding Modules}
+
+\begin{description}
+\item[Secrets:]The data structure and algorithm used to implement the virtual
+  hardware.
+\item[Services:]Serves as a virtual hardware used by the rest of the
+  system. This module provides the interface between the hardware and the
+  software. So, the system can use it to display outputs or to accept inputs.
+\item[Implemented By:] OS
+\end{description}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Example Modules from SWHS}
+
+\textbf{Input Verification Module}
+
+\begin{description}
+\item[Secrets:] The rules for the physical and software constraints.
+\item[Services:] Verifies that the input parameters comply with physical and
+  software constraints. Throws an error if a parameter violates a physical
+  constraint. Throws a warning if a parameter violates a software constraint.
+\item[Implemented By:] SWHS
+\end{description}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Example Modules from SWHS}
+
+\textbf{ODE Solver Module}
+
+\begin{description}
+\item[Secrets:] The algorithm to solve a system of first order ODEs.
+\item[Services:] Provides solvers that take the governing equation, initial
+  conditions, and numerical parameters, and solve them.
+\item[Implemented By:] Matlab
+\end{description}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}[plain, fragile]
+
+\frametitle{SWHS Uses Hierarchy}
+
+\begin{center}
+\includegraphics[scale=0.55]{UsesHierarchy.pdf}
+\end{center}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Modules with External Interaction}
+
+\begin{itemize}
+\item In general, some modules may interact with the environment or other modules
+%\item The Display Point Masses Applet module does this
+\item Environment might include the keyboard, the screen, the file system, motors, sensors, etc.
+\item Sometimes the interaction is informally specified using prose (natural language)
+\item Can introduce an environment variable
+\begin{itemize}
+\item Name, type
+\item Interpretation
+\end{itemize}
+\item Environment variables include the screen, the state of a motor (on, direction of rotation, power level, etc.),
+the position of a robot
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{External Interaction Continued}
+
+\begin{itemize}
+\item Some external interactions are hidden
+\begin{itemize}
+\item Present in the implementation, but not in the MIS
+\item An example might be OS memory allocation calls
+\end{itemize}
+\item External interaction described in the MIS
+\begin{itemize}
+\item Naming access programs of the other modules
+\item Specifying how the other module's state variables are changed
+\item The MIS should identify what external modules are used
+\end{itemize}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}
+\frametitle{MIS for GUI Modules}
+
+\begin{itemize}
+\item Could introduce an environment variable
+\item window: sequence [RES\_H][RES\_V] of pixelT
+\begin{itemize}
+\item Where window[r][c] is the pixel located at row r and column c, with numbering zero-relative and beginning at the
+upper left corner
+\item Would still need to define pixelT
+\end{itemize}
+\item Could formally specify the environment variable transitions
+\item More often it is reasonable to specify the transition in prose
+\item In some cases the proposed GUI might be shown by rough sketches
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Display Point Masses Module Syntax}
+
+\textbf{Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exc.}\\
+\hline
+DisplayPointMassesApplet & ~ & DisplayPointMassesApplet & ~\\
+\hline
+paint & ~ & ~ & ~\\
+\hline
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Display Point Masses Module Semantics}
+
+\textbf{Environment Variables}\\
+$\mathit{win}:$ 2D sequence of pixels displayed within a web-browser \\
+
+\noindent DisplayPointMassesApplet():
+\begin{itemize}
+\item transition: The state of the abstract object ListPointMasses is modified as follows:\\
+ListPointMasses.init()\\
+ListPointMasses.add(0, PointMassT(20, 20, 10)\\
+ListPointMasses.add(1, PointMassT(120, 200, 20)\\
+...
+\end{itemize}
+
+\noindent paint():
+\begin{itemize}
+\item transition $win := $ Modify window so that the point masses in ListPointMasses 
+are plotted as circles.  The centre of each circles should be the corresponding x and y coordinates and the radius should
+be the mass of the point mass.
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}
+\frametitle{Assignment 3 Vector Module}
+
+\textbf {Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | p{0.75in} |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+new vectorT & real $\rightarrow$ real & vectorT & ~\\
+\hline
+getf & ~ & real $\rightarrow$ real & ~\\
+\hline
+eval & real, real, integer & sequence of real & deltaNeg, nstepsNeg\\
+\hline
+evalPrint & real, real, integer & ~ & deltaNeg, nstepsNeg\\
+\hline
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Vector Module Semantics}
+
+\textbf{Environment Variables}\\
+$\mathit{screen}$ : two dimensional sequence of positions on the screen, which each position holding a character\\
+~\newline
+\textbf{State Variables}\\
+$f$: real $\rightarrow$ real\\
+~\newline
+\textbf{Access Routine Semantics}\\
+\noindent eval ($\mathit{startx}, \mathit{deltax}, \mathit{nsteps}$):
+\begin{itemize}
+\item output: $out := < f(\mathit{startx}), f(\mathit{startx} + \mathit{deltax}), f(\mathit{startx} + 2 \cdot \mathit{deltax}), ...
+, f(\mathit{startx} + \mathit{nsteps} \cdot \mathit{deltax})>$
+\item exception: $exc := ((\mathit{deltax} < 0) \Rightarrow  \mbox{deltaNeg} | (\mathit{nsteps} < 0) \Rightarrow
+\mbox{nstepsNeg})$
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Vector Module Semantics Continued}
+
+\noindent evalPrint ($\mathit{startx}, \mathit{deltax}, \mathit{nsteps}$):
+\begin{itemize}
+\item transition: The state of $\mathit{screen}$ is modified so that the sequence returned by eval ($\mathit{startx}$,
+$\mathit{deltax}$, $\mathit{nsteps}$) is displayed.
+\item exception: $exc := ((\mathit{deltax} < 0) \Rightarrow  \mbox{deltaNeg} | (\mathit{nsteps} < 0) \Rightarrow
+\mbox{nstepsNeg})$
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Dr.\ v.\ Mohrenschildt's Maze Tracing Robot Example}
+
+\begin{figure}
+\includegraphics[scale=0.42]{ExampleMaze.pdf}
+\end{figure}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Maze Tracing Robot Expected Changes}
+
+\begin{itemize}
+\item Changes to the geometry of the robot such that the mapping from a position to the robot inputs is different
+\item Changes to the interface to the robot
+\item Changes to the format of the maze
+\item Changes to any constant values
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Maze Tracing Robot Uses Hierarchy}
+
+\begin{figure}[H]
+\includegraphics[scale=0.42]{UsesHierarchyBetter.pdf}
+\end{figure}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Maze Tracing Robot MG}
+\begin{itemize}
+\item \structure<1>{Module name:} maze\_storage
+\begin{itemize}
+\item \structure<1>{Secret:} how the maze is stored
+\item \structure<1>{Service:} stores the maze
+\item \structure<1>{Module prefix:} ms\_
+\end{itemize}
+\item \structure<1>{Module name:} load\_maze
+\begin{itemize}
+\item \structure<1>{Secret:} where and how the maze file is read in
+\item \structure<1>{Service:} loads the maze
+\item \structure<1>{Module prefix:} lm\_
+\end{itemize}
+\item \structure<1>{Module name:} find\_path
+\begin{itemize}
+\item \structure<1>{Secret:} the algorithm for finding the shortest path
+\item \structure<1>{Service:} finds the shortest path through the maze
+\item \structure<1>{Module prefix:} fp\_
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Maze Tracing Robot MG Continued}
+\begin{itemize}
+\item \structure<1>{Module name:} control
+\begin{itemize}
+\item \structure<1>{Secret:} how the arm moves from position to position and how the buttons are checked
+\item \structure<1>{Service:} controls the movement of the arm
+\item \structure<1>{Module prefix:} cn\_
+\end{itemize}
+\item \structure<1>{Module name:} geometry
+\begin{itemize}
+\item \structure<1>{Secret:} how the calculations from cell coords to robot coords are performed
+\item \structure<1>{Service:} handles geometric positioning of the arm
+\item \structure<1>{Module prefix:} gm\_
+\end{itemize}
+\item \structure<1>{Module name:} hardware
+\begin{itemize}
+\item \structure<1>{Secret:} how it interfaces with the robot
+\item \structure<1>{Service:} handles hardware aspects of arm (movement and button checking)
+\item \structure<1>{Module prefix:} hw\_
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Maze Tracing Robot MG Continued}
+\begin{itemize}
+\item \structure<1>{Module name:} types\_constants
+\begin{itemize}
+\item \structure<1>{Secret:} how the data structures are defined and constants defined
+\item \structure<1>{Service:} provides standard variable types and constants to modules
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{maze\_storage MIS}
+
+\textbf{Module}\\
+~\newline
+maze\_storage\\
+~\newline
+
+\textbf{Uses}\\
+~\newline
+types\_constants\\
+~\newline
+
+\textbf{Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+... & ... & ... & ...\\
+\hline
+%any thoughts from the class on the design of the interface?
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}
+\frametitle{maze\_storage Exported Access Programs}
+
+\begin{tabular}{| l | l | l | p{3.5cm} |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+ms\_init & ~ & ~ & ~\\
+\hline
+ms\_set\_maze\_start & cell & ~ & ms\_not\_initialized, ms\_cell\_out\_of\_range\\
+\hline
+ms\_set\_maze\_end & cell & ~ & ms\_not\_initialized, ms\_cell\_out\_of\_range\\
+\hline
+ms\_get\_maze\_start & ~ & cell & ms\_not\_initialized\\
+\hline
+ms\_get\_maze\_end & ~ & cell & ms\_not\_initialized\\
+\hline
+ms\_set\_wall & cell, cell & ~ & ms\_not\_initialized, ms\_not\_valid\_wall\\
+\hline
+ms\_is\_connected & cell, cell & boolean & ms\_not\_initialized, ms\_cell\_out\_of\_range\\
+\hline
+\end{tabular}\\
+~\newline
+cell = tuple of (x: integer, y: integer)
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{maze\_storage Semantics}
+
+\textbf{State Variables}\\
+~\newline
+\uncover<2->{\structure<2>{$\mathit{maze}$: set of tuple of ( cell, cell )}}\\
+\uncover<2->{\structure<2>{$\mathit{start}: \mbox{cell} $}}\\
+\uncover<2->{\structure<2>{$\mathit{end}: \mbox{cell} $}}\\
+\uncover<2->{\structure<2>{$\mathit{is\_init}: \mbox{boolean} := \mathit{false}$}}\\
+
+~\newline
+\textbf{State Invariant:} none\\
+% there could be one related to maximum size of the map
+~\newline
+\textbf{Assumptions}\\
+~\newline
+ms\_get\_maze\_start and ms\_get\_maze\_end are not called until after the corresponding set routines have been called.
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics}
+
+\noindent ms\_init():
+\begin{itemize}
+\item transition: \uncover<2->{\structure<2>{$\mathit{maze}, \mathit{is\_init} := \{ \}, \mathit{true}$}}
+\item exception: \uncover<2->{\structure<2>{none}}
+\end{itemize}
+
+\noindent ms\_set\_maze\_start(c):
+\begin{itemize}
+\item transition: \uncover<3->{\structure<3>{$start := c$}}
+\item exception: \uncover<4->{\structure<4>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
+\mbox{ } \neg \mbox{cell\_in\_range}(c) \Rightarrow \mbox{ms\_cell\_out\_of\_range})$}}
+\end{itemize}
+
+\noindent ms\_set\_maze\_end(c):
+\begin{itemize}
+\item transition: \uncover<3->{\structure<3>{$end := c$}}
+\item exception: \uncover<4->{\structure<4>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
+\mbox{ } \neg \mbox{cell\_in\_range}(c) \Rightarrow \mbox{ms\_cell\_out\_of\_range})$}}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics Continued}
+
+\noindent ms\_get\_maze\_start():
+\begin{itemize}
+\item output: \uncover<2->{\structure<2>{$\mathit{out} := \mathit{start}$}}
+\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized})$}}
+\end{itemize}
+
+\noindent ms\_get\_maze\_end():
+\begin{itemize}
+\item output: \uncover<2->{\structure<2>{$\mathit{out} := \mathit{end}$}}
+\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized})$}}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics Continued}
+
+\noindent ms\_set\_wall(c1, c2):
+\begin{itemize}
+\item transition: \uncover<2->{\structure<2>{$\mathit{maze} := \mathit{maze} \cup \{ < c1, c2 > \}$}}
+\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
+\mbox{ wall\_is\_point}(c1, c2) \vee \mbox{wall\_is\_diagonal}(c1, c2) \vee \mbox{wall\_is\_out\_of\_range}(c1, c2)
+\Rightarrow \mbox{ms\_not\_valid\_wall})$}}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics Continued}
+
+\noindent ms\_is\_connected(c1, c2):
+\begin{itemize}
+\item output: \uncover<2->{\structure<2>{$out := < c1, c2 > \in \mathit{maze}$}}
+\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
+\mbox{ } \neg \mbox{cell\_in\_range}(c1) \Rightarrow \mbox{ms\_cell\_out\_of\_range } |
+\mbox{ } \neg \mbox{cell\_in\_range}(c2) \Rightarrow \mbox{ms\_cell\_out\_of\_range} )$}}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Local Functions}
+
+\noindent cell\_in\_range : cell $\rightarrow$ boolean
+\begin{itemize}
+\item \uncover<2->{\structure<2>{cell\_in\_range (c) $\equiv (0 \leq c.x < \mbox{MAX\_NUM\_CELLS}) \wedge (0 \leq c.y <
+\mbox{MAX\_NUM\_CELLS})$}}
+\end{itemize}
+
+\noindent wall\_is\_point: cell $\times$ cell $\rightarrow$ boolean
+\begin{itemize}
+\item \uncover<3->{\structure<3>{wall\_is\_point (c1, c2) $\equiv c1 = c2$}}
+\end{itemize}
+
+\noindent wall\_is\_diagonal: cell $\times$ cell $\rightarrow$ boolean
+\begin{itemize}
+\item \uncover<4->{\structure<4>{wall\_is\_diagonal (c1, c2) $\equiv \neg ( (c1.x = c2.x) \vee (c1.y = c2.y) )$}}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Additional Specifications for Determining the Path}
+
+pathT = sequence of cell\\
+~\newline
+
+\noindent validPath : pathT $\rightarrow$ boolean
+\begin{itemize}
+\item \uncover<2->{\structure<2>{validPath (p) $\equiv (p[0] = \mbox{ms\_get\_maze\_start}() 
+\wedge p[|p| - 1] = \mbox{ms\_get\_maze\_end}()
+\wedge \forall (i:\mathbb{N} | 0 \leq i \leq |p| - 2 : \mbox{ms\_is\_connected}(p[i], p[i+1]) )$}}
+\end{itemize}
+~\newline
+\uncover<3->{\structure<3>{How would you specify the length of a wall?}}\\
+\uncover<4->{\structure<4>{lengthWall: tuple of cell $\rightarrow$ integer}}\\
+\uncover<4->{\structure<4>{$$\mbox{lengthWall}(<c1, c2>) \equiv (c1.x = c2.x \Rightarrow | c1.y - c2.y |$$}}
+\uncover<4->{\structure<4>{$$ |  c1.y = c2.y \Rightarrow | c1.x - c2.x |)$$}}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Shortest Path}
+
+How would you specify the length of a path?\\
+\uncover<2->{\structure<2>{lengthPath: pathT $\rightarrow$ integer}}\\
+\uncover<2->{\structure<2>{$$\mbox{lengthPath}(p) \equiv + (i: \mathbb{N} | 0 \leq i < (|p| -1 ) : \mbox{lengthWall}(<p_i, p_{i+1} >))+1$$}}
+% the plus 1 is added because the length does not include the last point
+\noindent How would you specify whether a path is the shortest path?\\
+\uncover<3->{\structure<3>{isShortest: pathT $\rightarrow$ boolean}}\\
+\uncover<3->{\structure<3>{$$\mbox{isShortest}(p) = \forall ( q : \mbox{pathT} $$}}
+\uncover<3->{\structure<3>{$$|\mbox{validPath}(q) : \mbox{validPath}(p) \wedge \mbox{lengthPath}(p) \leq \mbox{lengthPath}(q))$$}}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
diff --git a/Lectures/L19_ModulesWithExternalInteraction/UsesHierarchy.pdf b/Lectures/L19_ModulesWithExternalInteraction/UsesHierarchy.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..a229222f5284ff31b7e96c88ae67d0c2a012bd50
Binary files /dev/null and b/Lectures/L19_ModulesWithExternalInteraction/UsesHierarchy.pdf differ
diff --git a/Lectures/L19_ModulesWithExternalInteraction/UsesHierarchyBetter.pdf b/Lectures/L19_ModulesWithExternalInteraction/UsesHierarchyBetter.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..1a9858ce5ca738b9024a8e773b77e5b03061ea83
Binary files /dev/null and b/Lectures/L19_ModulesWithExternalInteraction/UsesHierarchyBetter.pdf differ
diff --git a/ReferenceMaterial/ExampleMaze_FormalSpec.pdf b/ReferenceMaterial/ExampleMaze_FormalSpec.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..224e9ba24c2f23a5ec34190cbfa3cc03e3dafb11
Binary files /dev/null and b/ReferenceMaterial/ExampleMaze_FormalSpec.pdf differ
diff --git a/ReferenceMaterial/vMohrenshildtAndPeters1998.pdf b/ReferenceMaterial/vMohrenshildtAndPeters1998.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..8fa4769318305c6c857427fd85e1dd558f4e619e
Binary files /dev/null and b/ReferenceMaterial/vMohrenshildtAndPeters1998.pdf differ