Work on Tutorial (content and style)

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@11847 1434b563-b632-4741-aa49-43a3a8374d2e

org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css

@@ -285,6 +285,7 @@ p {
     margin-top: 0px;
     margin-bottom: 1em;
     text-align: justify;
+	font-family: Georgia;
 }
 
 img {
@@ -326,7 +327,7 @@ body {
 }
 
 /* (mj) Used for the Hint-Images */
-blockquote p img {
+blockquote p span.rmfamily img {
   float: left;
   position: absolute;
   left: 0.5em;

org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/styles/styles.css

@@ -286,6 +286,8 @@ p {
     margin-top: 0px;
     margin-bottom: 1em;
     text-align: justify;
+	font-family: Georgia;
+	font-size: 120%;
 }
 
 img {
@@ -355,8 +357,8 @@ color: #000;
 #navlist a:visited { color: #000; }
 
 /* (mj) Used for the Hint-Images */
-blockquote p img {
+blockquote p span.rmfamily img {
   float: left;
   position: absolute;
-  left: 12em;
+  left: 10em;
 }

org.rodinp.handbook.feature/latex/faq.tex

@@ -9,7 +9,7 @@ More details are available in \url{http://www.event-b.org}.
 
 \subsection{What is the difference between Event-B and the B method?}
 
-Event-B (\ref{event-b}) is derived from the B method. Both notations have the same inventor, and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose. The B method is devoted to the development of correct by construction software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation).
+Event-B (\ref{eventb}) is derived from the B method. Both notations have the same inventor, and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose. The B method is devoted to the development of correct by construction software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation).
 
 Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different).
 

org.rodinp.handbook.feature/latex/plastex-bsymb.sty

@@ -23,7 +23,7 @@
 \NeedsTeXFormat{LaTeX2e}[1999/06/01]
 \ProvidesPackage{bsymb}
    [2005/04/27 v1.5 Symbols for the B language]
-\RequirePackageWithOptions{amssymb}
+%%\RequirePackageWithOptions{amssymb}
 \newcommand\bsymb@defop[2]{
   \newcommand{#1}{\mathop{#2}\nolimits}
 }

org.rodinp.handbook.feature/latex/reference.tex

@@ -3,13 +3,31 @@
 \section{Arithmetic}
 \label{arithmetic}
 
+\section{Camille}
+\label{camille}
+
+Camille is an alternative, text-based editor.  It can be installed through the Eclipse Install mechanism.  More information is available in the Rodin Wiki (\ref{rodin_wiki}).
+
+\section{Context}
+\label{context}
+
+\section{Datatypes}
+\label{datatypes}
+
+List of Event-B datatypes
+
 \section{Eclipse}
 \label{eclipse}
 
 ... Eclipse Definition ...
 
+\section{Event}
+\label{event}
+
+Definition event
+
 \section{Event-B}
-\label{event-b}
+\label{eventb}
 
 Event-B is a formal method (\ref{formal_method}) for system-level modelling and analysis. Key features of Event-B are the use of set theory (\ref{set_theory}) as a modelling notation, the use of refinement (\ref{refinement}) to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
 
@@ -18,6 +36,16 @@ Event-B is a formal method (\ref{formal_method}) for system-level modelling and
 \item \url{http://www.event-b.org}
 \end{itemize}
 
+\section{Event-B Component}
+\label{eventb_component}
+
+Machines (\ref{machine}) and Contexts (\ref{context}) are components.
+
+\section{Event-B Explorer}
+\label{eventb_explorer}
+
+The View showing the Event-B projects and their content.  In the default Event-B perspective, it is the slim browser on the left edge of the Workspace.  If it is missing, make sure that you use the correct perspective.  You can explicitly enable it with \textsf{Windows $\rangle$ Show View... $\rangle$ Event-B Explorer}.
+
 \section{First Order Predicate Calculus}
 \label{first_order_predicate_calculus}
 
@@ -25,10 +53,26 @@ Event-B is a formal method (\ref{formal_method}) for system-level modelling and
 \section{Formal Method}
 \label{formal_method}
 
+\section{Guard}
+\label{guard}
+
 \section{IDE}
 \label{ide}
 
-... IDE Definition ...
+Integrated Development Environment
+
+\section{Initialization}
+\label{initialization}
+
+Every machine has a special event \texttt{INITIALIZATION} that will be used to initialize the machine's state.
+
+TODO: Determinism, refinement.
+
+\section{Label}
+\label{label}
+
+\section{Machine}
+\label{machine}
 
 \section{Naming Convention}
 \label{naming_convention}
@@ -38,22 +82,31 @@ In this section we describe a recommended naming convention.  Good naming conven
 \section{Refinement}
 \label{refinement}
 
-... Refinement Definition ...
-
-\subsection{Horizontal Refinement}
-\label{horizontal_refinement}
-
-\subsection{Vertical Refinement}
-\label{vertical_refinement}
-
-\subsection{Data Refinement}
-\label{data_refinement}
+\begin{description}
+	\item[Horizontal Refinement]
+	\item[Vertical Refinement]
+	\item[Data Refinement]
+\end{description}
 
 \paragraph*{See also:}
 \begin{itemize}
 \item Data refinement in the trafficlight tutorial (\ref{tutorial_tl_data_refinement})
 \end{itemize}
 
+\section{Rodin Wiki}
+\label{rodin_wiki}
+
+\url{http://wiki.event-b.org/}
+
+\section{Structural Editor}
+\label{structural_editor}
+
+\section{Project}
+\label{project}
+
+\section{Proof Obligation Labels}
+\label{po_labels}
+
 \section{Propositional Calculus}
 \label{propositional_calculus}
 
@@ -62,10 +115,22 @@ In this section we describe a recommended naming convention.  Good naming conven
 
 ... Rodin Definition ...
 
+
 \section{Rodin Platform}
 \label{rodin_platform}
 
-... Rodin Platform Definition ...
+\section{Rodin Problems View}
+\label{rodin_problems_view}
+
+
+\section{Rodin Nature}
+\label{rodin_nature}
+
+Eclipse Projects can have one or more natures to describe their purpose.  The GUI can then adapt to their nature.  Rodin Projects must have the Rodin-Nature.  If you create an Event-B project, it automatically has the right nature.  If you want to modify an existing project, you can edit the \texttt{.project} file and add the following XML in the \texttt{<natures>} section:
+
+\pencil{
+\texttt{<nature>org.rodinp.core.rodinnature</nature>}
+}
 
 \section{Set Theory}
 \label{set_theory}

org.rodinp.handbook.feature/latex/rodin-doc.tex

 \documentclass{book}
+\usepackage[left=2.5cm,top=3cm,right=2.5cm,bottom=3cm]{geometry}
 \usepackage{hyperref}
 \usepackage{graphicx}
 \usepackage{bsymb}
 \usepackage{b2latex}
 \usepackage{fancyhdr,lastpage,color}
-\usepackage[left=2.5cm,top=3cm,right=2.5cm,bottom=3cm]{geometry}
-
 
 \def\doculist#1#2{
 \begin{quote}
 \hspace{-10mm}
-\includegraphics[width=7mm]{#2}
+\textrm{\includegraphics[width=7mm]{#2}} % Hack!  We "mark" the image with textrm so that we can use a different CSS-Style in plastex.
 \vspace{-8mm}
 
 #1
@@ -47,11 +46,11 @@ We decided on the following approach:
 
 This document demonstrates this approach with a very small portion of the existing Rodin documentation.  Obviously, it is just a proof of concept.
 
-\subsection{Foreword}
+\section{Foreword}
 
 By Cliff and/or Jean-Raymond.
 
-\subsection{Conventions}
+\section{Conventions}
 
 We use the following conventions in this manual:
 
@@ -60,9 +59,12 @@ We use the following conventions in this manual:
 \warning{Potential problems and warnings are designated by a warning sign.}
 \pencil{Examples and Code are designated by a pencil.}
 
-We use \texttt{typewriter} font for filenames and directories
+We use \texttt{typewriter} font for filenames and directories.
+
+We use \textsf{sans serif font} for GUI elements like menus and buttons.  Menu actions are depicted by a chain of elements, separated by ``$\rangle$'', e.g. \textsf{File $\rangle$ New $\rangle$ Event-B Component}.
+
 
-\subsection{Creative Commons License}
+\section{Creative Commons License}
 
 \input{style-guide}
 

org.rodinp.handbook.feature/latex/tutorial-03.tex

+\section{The First Machine: A Traffic Light Controller}
+\label{tutorial_3}
+
+% a first machine, e.g. a traffic light with booleans for signals.  We introduce guards, resulting in the proof obligations to be discharged automatically. We explain how proof lables are read, without changing to the proof perspective.
+
+\tick{\textbf{Goals:} The objective of this section is to get acquainted with the modeling environment. We will create a very simple model consisting of just one file to develop a feel for Rodin and Event-B.}
+
+In this tutorial, we will create a model of a traffic light controller.  We will use this example in repeatedly in subsequent Sections.  The following image depicts what we are trying to achieve:
+
+\begin{center}
+	\includegraphics[width=0.7\textwidth]{img/tutorial/trafficlight.png}
+\end{center}
+
+In this Section, we will implement a simplified controller with the following differences:
+\begin{itemize}
+	\item We model the signals with booleans to indicated ``stop'' (false) and ``go''.  We do not model colors (yet).
+	\item We do not model the push button yet.
+\end{itemize}
+
+\subsection{Project Setup}
+
+Models typically consist of multiple files that are managed in a Project (\ref{project}).  Create a new Event-B Project \textsf{File $\rangle$ New $\rangle$ Event-B Project}.  Give the project the name \texttt{tutorial-03}.
+
+\warning{Eclipse supports different types of Projects.  The Project must have the Rodin Nature (\ref{rodin_nature}) to work.  A project can have more than one nature.}
+
+Next, create a new Event-B Component (\ref{eventb_component}).  Either use \textsf{File $\rangle$ New $\rangle$ Event-B Component}, or right-click on the newly created project and select \textsf{New $\rangle$ Event-B Component}.  Use \texttt{mac} as the component name and click \textsf{Finish}.  This will create a Machine (\ref{machine}) file.
+
+The newly created Component will open in the structural editor (\ref{structural_editor}).  The editor has four tabs at the bottom.  The \textsf{Pretty Print} shows the model as a whole with color highlighting, but it cannot be edited here.  This is useful to inspect the model.  The \textsf{Edit} allows editing of the model.  It shows the six main sections of a machine (REFINES, SEES, etc.) in a collapsed state.  You can click on the little triangle to the left of a section to expand it.
+
+The editor is \textit{form-based}.  This means that in well-defined places an appropriate control (text field, dropdown, etc.) allows modifications.
+
+\info{Alternative editors are available as plug-ins.  The form editor has the advantage of guiding the user through the model, but it takes up a lot of real estate and can be slow on big models.  The text- based Camille Editor (\ref{camille}) is very popular.  Please visit the Rodin Wiki (\ref{rodin_wiki}) for the latest information.}
+
+
+\subsection{Building the Model}
+
+Back to the problem: Our objective is to build a simplified traffic light controller, as described in \ref{tutorial_3}.  We start with the model state.  We will model two traffic lights.  Therefore, we will create two variables, called \texttt{cars\_go} and \texttt{peds\_go}.  Go to the \textsf{Edit} tab in the editor and expand the \textsf{VARIABLES} section.  Click on the green plus-sign to create a new variable.
+
+\subsubsection{Creating Variables}
+
+You will see two fields, the left one prepopulated with \texttt{var1}.  Change this to \texttt{cars\_go}.  The second field (after the double-slash ``//'') is a comment field that can take any text.
+
+\info{\textbf{Comments:} The comment field supports line breaks.  Note that it is not possible to ``comment out'' parts of the model, as you would expect in programming languages.  You can use the comment field to ``part'' predicates and other strings temporarily.}
+
+Create the second variable (\texttt{peds\_go}) correspondingly.  Your editor should now look as follows:
+
+TODO: Screenshot
+
+Upon saving, the variables will be highlighted in red, indicating a problem.  The \textsf{Rodin Problems} View (\ref{rodin_problems_view}) shows corresponding error messages, in this case ``Variable cars\_go does not have a type''.
+
+Types are provided by invariants.  Corresponding the the steps above, expand the \textsf{INVARIANTS} section and add two elements.  Invariants have labels (\ref{label}).  Default labels are generated (\texttt{inv1} and \texttt{inv2}).  The actual invariant is prepopulated with $\btrue$, representing logical true.  Change this to $cars\_go \in  BOOL$.  Event-B provides the build-in datatype \texttt{BOOL}, amongst others (\ref{datatypes}).
+
+\info{\textbf{Mathematical Symbols:} Every mathematical symbol has an ASCII-representation that is substituted automatically.  To generate ``element of'' ($\in$), simply type a colon (``:'').  The editor will perform the substitution after a short delay.  The symbol view shows all supported mathematical symbols.  The symbol view discloses the ASCII representation by hovering over the symbol in question.}
+
+After saving, you should see that the \textsf{EVENTS} section is highlighted in yellow.  Again, the \textsf{Rodin Problems} View gives us the reason: ``Variable cars\_go is not initialized''.  Every variable must be initialized in a way that is consistent with the model.
+
+To fix this problem, expand the \textsf{EVENTS} and in turn the INITIALIZATION event (\ref{initialization}).  Add two elements in the \textsf{THEN} block.  These are actions that also have labels.  In the action fields, provide $cars\_go :=  FALSE$ and $peds\_go :=  FALSE$.
+
+\subsubsection{State Transitions with Events}
+
+Our traffic light controller cannot yet change its state.  To make this possible, we provide events (\ref{event}). We start with the traffic light for the pedestrians, and we will provide two events, one to set it to ``go'' and one to set it to ``stop''.
+
+\warning{From now on, we won't describe the individual steps in the editor any more.  Instead, we will simply show the resulting model.} 
+
+The two events will look as follows:
+
+\pencil{
+\begin{description}
+	\EVT {set\_peds\_go}
+		\begin{description}
+		\BeginAct
+			\begin{description}
+			\nItemX{ act1 }{ peds\_go :=  TRUE }
+			\end{description}
+		\EndAct
+		\end{description}
+	\EVT {set\_peds\_stop}
+		\begin{description}
+		\BeginAct
+			\begin{description}
+			\nItemX{ act1 }{ peds\_go :=  FALSE }
+			\end{description}
+		\EndAct
+		\end{description}
+\end{description}
+}
+
+\subsubsection{Event parameters}
+
+For the traffic light for the cars, we will present a different approach and use only one event with a parameter.  The event will use the new traffic light state as the argument.  The parameter is declared in the \textsf{any} section and typed in the \textsf{where} section:
+
+\pencil{
+\begin{description}
+	\EVT {set\_cars}
+		\begin{description}
+		\AnyPrm
+			\begin{description}
+			\ItemX{ new\_value }
+			\end{description}
+		\WhereGrd
+			\begin{description}
+			\nItemX{ grd1 }{ new\_value \in  BOOL }
+			\end{description}
+		\ThenAct
+			\begin{description}
+			\nItemX{ act1 }{ cars\_go :=  new\_value }
+			\end{description}
+		\EndAct
+		\end{description}
+\end{description}
+}
+
+Note how the parameter is used in the action block.
+
+\subsubsection{Invariants}
+
+If this model would control a traffic light, we would have a problem, as nothing is preventing the model from setting both traffic lights to \texttt{TRUE}.  The reason is that so far we only modeled the domain (the traffic lights and their states), and not the requirements.  We have the following safety requirement:
+
+\begin{center}REQ-1: Both traffic lights must not be \texttt{TRUE} at the same time.\end{center}
+
+We can model this requirement with the following invariant (please add this invariant to the model):
+\[
+\lnot  (cars\_go = TRUE \land  peds\_go = TRUE)
+\]
+
+Obviously, this invariant can be violated, and Rodin can tell us that.  The Explorer (\ref{eventb_explorer}) provides this information in various ways.  Go to the explorer and expand the project (\texttt{tutorial-03}), the machine (\texttt{mac}) and the entry ``Proof Obligations''.  You should see four proof obligations, two of which are not discharged.
+
+\info{Make sure that you understand the proof obligation labels (\ref{po_labels}).  Also, the proof obligations can also be found via other entries.  Elements that have non-discharged proof obligations as children are marked with a small question mark.  For instance, \texttt{inv3} has all proof obligations as children, while the event \texttt{set\_cars} has one.}
+
+To prevent the invariant from being violated (and therefore to allow all proof obligations to be discharged), we need to strengthen the guards (\ref{guard}) of the events.
+
+\warning{Before looking at the solution, try to fix the model yourself.}
+
+This concludes the tutorial.
+
+\subsection{The Final Traffic Light Model}
+
+\pencil{
+\begin{description}
+\MACHINE{mac}
+\VARIABLES
+	\begin{description}
+		\Item{ cars\_go }
+		\Item{ peds\_go }
+	\end{description}
+\INVARIANTS
+	\begin{description}
+		\nItemX{ inv1 }{ cars\_go \in  BOOL }
+		\nItemX{ inv2 }{ peds\_go \in  BOOL }
+		\nItemX{ inv3 }{ \lnot  (cars\_go = TRUE \land  peds\_go = TRUE) }
+	\end{description}
+\EVENTS
+	\INITIALISATION
+		\begin{description}
+		\BeginAct
+			\begin{description}
+			\nItemX{ act1 }{ cars\_go :=  FALSE }
+			\nItemX{ act2 }{ peds\_go :=  FALSE }
+			\end{description}
+		\EndAct
+		\end{description}
+	\EVT {set\_peds\_go}
+		\begin{description}
+		\WhenGrd
+			\begin{description}
+			\nItemX{ grd1 }{ cars\_go = FALSE }
+			\end{description}
+		\ThenAct
+			\begin{description}
+			\nItemX{ act1 }{ peds\_go :=  TRUE }
+			\end{description}
+		\EndAct
+		\end{description}
+	\EVT {set\_peds\_stop}
+		\begin{description}
+		\BeginAct
+			\begin{description}
+			\nItemX{ act1 }{ peds\_go :=  FALSE }
+			\end{description}
+		\EndAct
+		\end{description}
+	\EVT {set\_cars}
+		\begin{description}
+		\AnyPrm
+			\begin{description}
+			\ItemX{ new\_value }
+			\end{description}
+		\WhereGrd
+			\begin{description}
+			\nItemX{ grd1 }{ new\_value \in  BOOL }
+			\nItemX{ grd2 }{ new\_value = TRUE \limp  peds\_go = FALSE }
+			\end{description}
+		\ThenAct
+			\begin{description}
+			\nItemX{ act1 }{ cars\_go :=  new\_value }
+			\end{description}
+		\EndAct
+		\end{description}
+\END
+\end{description}
+}
+

org.rodinp.handbook.feature/latex/tutorial.tex

@@ -28,165 +28,6 @@ These are the chapters of the tutorial.  Average time available to write each ch
 	\item[Outlook] -- This concludes the tutorial, but we will provide many pointers to the user.  In particular, we will point to the literature from the deploy project, the Wiki and to plugins that solve specific problems.
 \end{description}
 
-\section{Theory to Get You Started}
-\label{tutorial_theory}
-
-\tick{\textbf{Goals:} The focus of this section is to briefly cover all the required theory, and to provide pointers for further reading.  Specifically, this includes Propositional Calculus, First Order Predicate Calculus, Set Theory and Arithmetic}
-
-\paragraph{See Also:}
-\begin{itemize}
-\item Mathematical Notation Slides \url{files/sld_mth1.pdf}
-\end{itemize}
-
-
-\section{Getting around Rodin}
-\label{tutorial_2}
-
-\tick{\textbf{Goals:} In this section, we cover installation, the basic features of an Eclipse application, and the Rodin-specific GUI elements.}
-
-
-\section{Example 1: A Trafficlight Controller}
-\label{tutorial_3}
-
-\tick{\textbf{Goals:} The focus of this section is modeling.  You will learn how to model a simple system (a traffic light controller).  We will use this example to introduce the concept of refinement (\ref{refinement}).  The proofs in this section should all be discharged automatically. }
-
-The following picture visualizes the problem we are going to solve:
-
-\begin{center}
-	\includegraphics[width=0.9\textwidth]{img/tutorial/trafficlight.png}
-\end{center}
-
-The objective is to design the software for a controller that switches the trafficlights and that reacts to pedestrian requests to cross the street.
-
-We tackle the problem in multiple steps:
-
-\begin{enumerate}
-	\item We will abstract the problem and develop a refinement plan (\ref{tutorial_tl_problem_abstraction})
-	\item We will implement the initial model (\ref{tutorial_tl_initial_model})
-	\item We will perform Data Refinement (\ref{data_refinement})
-\end{enumerate}
-
-\subsection{Problem Abstraction}
-\label{tutorial_tl_problem_abstraction}
-
-\subsection{Initial Model}
-\label{tutorial_tl_initial_model}
-
-\subsubsection{Project Setup}
-
-First create a new Event-B Project \textsf{File $\rangle$ New $\rangle$ Event-B Project}.  Give the project the name \texttt{trafficlight}.
-
-Next, create a Machine.  Right-click the newly created project and select \textsf{New $\rangle$ Event-B Component}.  Call the component \texttt{mac0}.
-
-\info{A good naming convention can save a lot of work.  We have a recommended naming convention (\ref{naming_convention})}
-
-\subsubsection{System State}
-
-We will now add the variables that store the traffic light value as a boolean.
-
-\tick{A new variable requires three elements: The variable itself, the typing invariant and the initialization.  But typically, we'd also add events that change the state.  And there may be further invariants constraining the state.}
-
-
-
-\pencil{
-\begin{description}
-\VARIABLES
-	\begin{description}
-		\Item{ cars\_go }
-	\end{description}
-\INVARIANTS
-	\begin{description}
-		\nItemX{ inv1 }{ cars\_go \in  BOOL }
-	\end{description}
-\EVENTS
-	\INITIALISATION
-		\begin{description}
-		\BeginAct
-			\begin{description}
-			\nItemX{ act1 }{ cars\_go :=  FALSE }
-			\end{description}
-		\EndAct
-		\end{description}
-\END
-\end{description}
-}
-
-
-\info{There are various ways to accelerate the creation of variables.  The structural editor has a wizard for this purpose.}
-
-\pencil{
-\begin{description}
-\MACHINE{mac0}
-\VARIABLES
-	\begin{description}
-		\Item{ cars\_go }
-		\Item{ peds\_go }
-	\end{description}
-\INVARIANTS
-	\begin{description}
-		\nItemX{ inv1 }{ cars\_go \in  BOOL }
-		\nItemX{ inv2 }{ peds\_go \in  BOOL }
-		\nItemX{ inv3 }{ \lnot  (cars\_go = TRUE \land  peds\_go = TRUE) }
-	\end{description}
-\EVENTS
-	\INITIALISATION
-		\begin{description}
-		\BeginAct
-			\begin{description}
-			\nItemX{ act1 }{ cars\_go :=  FALSE }
-			\nItemX{ act2 }{ peds\_go :=  FALSE }
-			\end{description}
-		\EndAct
-		\end{description}
-	\EVT {cars\_light}
-		\begin{description}
-		\AnyPrm
-			\begin{description}
-			\ItemX{ new\_value }
-			\end{description}
-		\WhereGrd
-			\begin{description}
-			\nItemX{ grd1 }{ \lnot  (new\_value = TRUE \land  peds\_go = TRUE) }
-			\end{description}
-		\ThenAct
-			\begin{description}
-			\nItemX{ act1 }{ cars\_go :=  new\_value }
-			\end{description}
-		\EndAct
-		\end{description}
-	\EVT {peds\_light}
-		\begin{description}
-		\AnyPrm
-			\begin{description}
-			\ItemX{ new\_value }
-			\end{description}
-		\WhereGrd
-			\begin{description}
-			\nItemX{ grd1 }{ \lnot  (cars\_go = TRUE \land  new\_value = TRUE) }
-			\end{description}
-		\ThenAct
-			\begin{description}
-			\nItemX{ act1 }{ peds\_go :=  new\_value }
-			\end{description}
-		\EndAct
-		\end{description}
-\END
-\end{description}
-}
-
-\subsection{Data Refinement: Introduce Trafficlight Colors}
-\label{tutorial_tl_data_refinement}
-
-
-- simple proofs
-- refinement
-
-\section{Excurs: Data Structures}
-\label{tutorial_4}
-
-\section{Excurs: Proofing}
-\label{tutorial_5}
-
-\section{A more complex Example}
+\input{tutorial-03}