Skip to content
Snippets Groups Projects
Commit 268a2aa9 authored by Michael Jastram's avatar Michael Jastram
Browse files

Initial import of Rodin Handbook Project.

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@11749 1434b563-b632-4741-aa49-43a3a8374d2e
parent 0bbba644
No related branches found
No related tags found
No related merge requests found
Showing
with 848 additions and 0 deletions
%-------------------------------------------------------------------
% This is b2latex.sty, generated by B2Latex plugin on Rodin
% Author: K. DAMCHOOM, kd06r@ecs.soton.ac.uk
% Copyright(c)2008 ECS @ University of Southampton
%-------------------------------------------------------------------
% This style file is required for all latex files generated by the
% B2Latex plugin 0.5.x.
% Each command mentioned below, can be modified for your own style
% but command names are not allowed.
%
%-------------------------------------------------------------------
% Defined colors.
%-------------------------------------------------------------------
\usepackage{color}
\definecolor{keycolor}{rgb}{0,0,0.7} %color of key words, blue is the default
\definecolor{labelcolor}{rgb}{0,0.4,0.8} %color of labels, cyan
\definecolor{codecolor}{rgb}{0,0.2,0} %color of formulas, black
\definecolor{xcodecolor}{rgb}{0,0,0} %color of extended formulas, black
\definecolor{cmtcolor}{rgb}{0,0,0} %color of comments, black
%-------------------------------------------------------------------
\newcommand{\paraSpc} {\hspace*{\fill} \setlength{\parskip}{-2pt}} % reduce space between paras
%-------------------------------------------------------------------
\newcommand{\itemSpc} {\setlength{\itemsep}{-0pt}} % reduce space between para items
%-------------------------------------------------------------------
% Special commands for MACHINE
%-------------------------------------------------------------------
\newcommand{\MACHINE}[1] { \item[\textcolor{keycolor}{MACHINE }] #1 \paraSpc }
\newcommand{\REFINES}[1]{ \item[\textcolor{keycolor}{REFINES }] #1 \paraSpc }
\newcommand{\SEES}[1]{ \item[\textcolor{keycolor}{SEES }] #1 \paraSpc }
\newcommand{\VARIABLES}{\item[\textcolor{keycolor}{VARIABLES}] \paraSpc }
\newcommand{\INVARIANTS}{ \item[\textcolor{keycolor}{INVARIANTS}] \paraSpc }
\newcommand{\VARIANT}{ \item[\textcolor{keycolor}{VARIANT}] \paraSpc }
\newcommand{\EVENTS}{ \item[\textcolor{keycolor}{EVENTS}] \paraSpc }
\newcommand{\INITIALISATION}{ \item[\textcolor{keycolor}{Initialisation}] \paraSpc }
\newcommand{\EVT}[1]{ \item[\textcolor{keycolor}{Event }] \textit{#1} $\defi$ \paraSpc } % opt1
% Option: deactivate above command and reactivate
% the command below to display only event name
%\newcommand{\EVT}[1]{ \item[\textit{#1}] $\defi$ \paraSpc } % opt2
\newcommand{\REF}[1]{ \item[\textcolor{keycolor}{refines}] \textit{#1} \paraSpc }
\newcommand{\EXTD}[1]{ \item[\textcolor{keycolor}{extends}] \textit{#1} \paraSpc }
\newcommand{\Status}[1]{ \item[\textcolor{keycolor}{Status}] #1 \paraSpc }
\newcommand{\AnyPrm}{ \item[\textcolor{keycolor}{any}] \paraSpc \itemSpc }
\newcommand{\WhereGrd}{ \item[\textcolor{keycolor}{where}] \paraSpc \itemSpc }
\newcommand{\WhenGrd}{ \item[\textcolor{keycolor}{when}] \paraSpc \itemSpc }
\newcommand{\Witnesses}{ \item[\textcolor{keycolor}{with}] \paraSpc \itemSpc }
\newcommand{\ThenAct}{ \item[\textcolor{keycolor}{then}] \paraSpc \itemSpc }
\newcommand{\BeginAct}{ \item[\textcolor{keycolor}{begin}] \paraSpc \itemSpc }
\newcommand{\EndAct}{ \item[\textcolor{keycolor}{end}] \paraSpc }
%-------------------------------------------------------------------
% Special commands for CONTEXT
%-------------------------------------------------------------------
\newcommand{\CONTEXT}[1]{ \item[\textcolor{keycolor}{CONTEXT }] #1 \paraSpc }
\newcommand{\EXTENDS}[1]{ \item[\textcolor{keycolor}{EXTENDS }] #1 \paraSpc }
\newcommand{\SETS}{ \item[\textcolor{keycolor}{SETS}] \paraSpc }
\newcommand{\CONSTANTS}{ \item[\textcolor{keycolor}{CONSTANTS}] \paraSpc }
\newcommand{\THEOREMS}{ \item[\textcolor{keycolor}{THEOREMS}] \paraSpc }
\newcommand{\AXIOMS}{ \item[\textcolor{keycolor}{AXIOMS}] \paraSpc }
%-------------------------------------------------------------------
% General commands used in both machines and contexts
%-------------------------------------------------------------------
% Specification Title
\newcommand{\BTitle}[3]{
\item[\fbox{\parbox{6in}{\centering{~\\An Event-B Specification of #1
\\Creation Date: #2 @ #3\\}}}]
}
% End of MACHINE or CONTEXT
\newcommand{\END}{ \item[\textcolor{keycolor}{END}] \hspace*{\fill} }
% Printing non-labelled elements
% (i.e. variables, sets and constants)
\newcommand{\Item}[1]{ \item[\textcolor{codecolor}{$\tt#1$}] \itemSpc }
\newcommand{\ItemX}[1]{ \item[\textcolor{xcodecolor}{$\it#1$}] \itemSpc }
% Printing an element with label name
% (i.e. invariants, theorems, axioms, witnesses and actions)
% parameter #1 is a label name and #2 is its content
\newcommand{\nItem}[2]{ \item[\textcolor{labelcolor}{$\tt #1:$}] \textcolor{codecolor}{$\tt #2$} \itemSpc } % opt1
\newcommand{\nItemX}[2]{ \item[\textcolor{labelcolor}{$\tt #1:$}] \textcolor{xcodecolor}{$\it #2$} \itemSpc } % opt1
% Below is an alternative command for printing with no label
%\newcommand{\nItem}[2]{ \item[] $#2$} % opt2
% Commentations, reselect the second option for displaying asterisks
% - Newline comment
\newcommand{\cmt}[1]{ \hspace*{\fill}\\\textcolor{cmtcolor}{ #1}} %opt1
%\newcommand{\cmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt2
% - Back Comment, for variables, sets and constants
\newcommand{\bcmt}[1]{~~~ \textcolor{cmtcolor}{#1}} %opt1
%\newcommand{\bcmt}[1]{~~~ $/\ast$ #1 $\ast/$} %opt2
% Select opt3 or opt4 (including asterisks) if you want to display this kind of comments
% on the newline like the newline comment
%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ #1} %opt3
%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt4
%-------------------------------------------------------------------
%%
%% This is file `bsymb.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% bsymb.dtx (with options: `package')
%%
%% This is a generated file.
%%
%% Copyright (C) 2004 by Laurent Voisin <laurent.voisin at inf.ethz.ch>
%%
%% This file may be distributed and/or modified under the
%% conditions of the LaTeX Project Public License, either version 1.3
%% of this license or (at your option) any later version.
%% The latest version of this license is in:
%%
%% http://www.latex-project.org/lppl.txt
%%
%% and version 1.3 or later is part of all distributions of LaTeX
%% version 2003/12/01 or later.
%%
\NeedsTeXFormat{LaTeX2e}[1999/06/01]
\ProvidesPackage{bsymb}
[2005/04/27 v1.5 Symbols for the B language]
\RequirePackageWithOptions{amssymb}
\newcommand\bsymb@defop[2]{
\newcommand{#1}{\mathop{#2}\nolimits}
}
\newcommand\bsymb@deford[2]{
\newcommand{#1}{\mathord{#2}}
}
\bsymb@deford{\bfalse}{\bot}
\bsymb@deford{\btrue}{\top}
\newcommand{\limp}{\mathbin\Rightarrow}
\newcommand{\leqv}{\mathbin\Leftrightarrow}
\bsymb@deford{\qdot}{\mkern1mu\cdot\mkern1mu}
\newcommand\defi{\mathrel{\widehat=}}
\bsymb@defop{\pow}{\mathbb P\hbox{}}
\bsymb@defop{\pown}{\mathbb P_1}
\newcommand{\cprod}{\mathbin\times}
\newcommand{\bunion}{\mathbin{\mkern1mu\cup\mkern1mu}}
\newcommand{\binter}{\mathbin{\mkern1mu\cap\mkern1mu}}
\bsymb@defop{\union}{\mathrm{union}}
\bsymb@defop{\inter}{\mathrm{inter}}
\newcommand{\Union}{\bigcup\nolimits}
\newcommand{\Inter}{\bigcap\nolimits}
\renewcommand{\emptyset}{\mathord\varnothing}
\newcommand{\rel}{\mathbin\leftrightarrow}
\newcommand{\trel}{\mathbin{\leftarrow\mkern-14mu\leftrightarrow}}
\newcommand{\srel}{\mathbin{\leftrightarrow\mkern-14mu\rightarrow}}
\newcommand{\strel}{\mathbin{\leftrightarrow\mkern-14mu\leftrightarrow}}
\bsymb@defop{\dom}{\mathrm{dom}}
\bsymb@defop{\ran}{\mathrm{ran}}
\newcommand{\fcomp}{\mathbin;}
\newcommand{\bcomp}{\circ}
\bsymb@defop{\id}{\mathrm{id}}
\newcommand{\domres}{\mathbin\lhd}
\newcommand{\domsub}{\mathbin{\lhd\mkern-14mu-}}
\newcommand{\ranres}{\mathbin\rhd}
\newcommand{\ransub}{\mathbin{\rhd\mkern-14mu-}}
\newcommand{\ovl}{\mathbin{\lhd\mkern-9mu-}}
\newcommand{\dprod}{\mathbin\otimes}
\bsymb@defop{\prjone}{\mathrm{prj}_1}
\bsymb@defop{\prjtwo}{\mathrm{prj}_2}
\newcommand{\pprod}{\mathbin\|}
\newcommand{\bsymb@partial}[2]{
\mathbin{\mkern#2mu\mapstochar\mkern-#2mu#1}
}
\newcommand{\pfun}{\bsymb@partial\rightarrow6}
\newcommand{\tfun}{\mathbin\rightarrow}
\newcommand{\pinj}{\bsymb@partial\rightarrowtail9}
\newcommand{\tinj}{\mathbin\rightarrowtail}
\newcommand{\psur}{\bsymb@partial\twoheadrightarrow6}
\newcommand{\tsur}{\mathbin\twoheadrightarrow}
\newcommand{\tbij}{\mathbin{
\rightarrowtail
\mkern-18mu\twoheadrightarrow}
}
\bsymb@defop{\fin}{\mathbb F\hbox{}}
\bsymb@defop{\finn}{\mathbb F_1}
\bsymb@deford{\nat}{\mathbb N}
\bsymb@deford{\natn}{\mathbb N_1}
\bsymb@deford{\intg}{\mathbb Z}
\bsymb@defop{\card}{\mathrm{card}}
\newcommand{\upto}{\mathbin{.\mkern1mu.}}
\bsymb@defop{\upred}{\mathrm{pred}}
\bsymb@defop{\usucc}{\mathrm{succ}}
\newcommand\expn{\mathbin{\widehat{\enskip}}}
\bsymb@deford{\Bool}{\mathrm{BOOL}}
\bsymb@deford{\True}{\mathrm{TRUE}}
\bsymb@deford{\False}{\mathrm{FALSE}}
\bsymb@defop{\bool}{\mathrm{bool}}
\newcommand{\bcmeq}{\mathrel{:\mkern1mu=}}
\newcommand{\bcmin}{\mathrel{:\mkern1mu\in}}
\newcommand{\bcmsuch}{\mathrel{:\mkern1mu\mid}}
\endinput
%%
%% End of file `bsymb.sty'.
\chapter{Frequently Asked Questions}
\section{General Questions}
\subsection{What is Event-B?}
Event-B is a formal method for system-level modelling and analysis. Key features of event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
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).
Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different).
\subsection{What is Rodin?}
The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
\subsection{Where does the Rodin name come from?}
The Rodin Platform (\ref{rodin_platform}) was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” . Rodin is also the name of a famous French sculptor, one of his most famous work being the Thinker.
\section{Installation Questions}
\section{Proofer Questions}
\section{Usage Questions}
\section{Plug-In Questions}
File added
org.rodinp.handbook.feature/latex/img/info_64.png

6.3 KiB

org.rodinp.handbook.feature/latex/img/pencil_64.png

6.52 KiB

org.rodinp.handbook.feature/latex/img/tick_64.png

5.83 KiB

org.rodinp.handbook.feature/latex/img/tutorial/trafficlight.png

6.72 KiB

org.rodinp.handbook.feature/latex/img/warning_64.png

5.12 KiB

%-------------------------------------------------------------------
% This is b2latex.sty, generated by B2Latex plugin on Rodin
% Author: K. DAMCHOOM, kd06r@ecs.soton.ac.uk
% Copyright(c)2008 ECS @ University of Southampton
%-------------------------------------------------------------------
% This style file is required for all latex files generated by the
% B2Latex plugin 0.5.x.
% Each command mentioned below, can be modified for your own style
% but command names are not allowed.
%
%-------------------------------------------------------------------
% Defined colors.
%-------------------------------------------------------------------
\usepackage{color}
\definecolor{keycolor}{rgb}{0,0,0.7} %color of key words, blue is the default
\definecolor{labelcolor}{rgb}{0,0.4,0.8} %color of labels, cyan
\definecolor{codecolor}{rgb}{0,0.2,0} %color of formulas, black
\definecolor{xcodecolor}{rgb}{0,0,0} %color of extended formulas, black
\definecolor{cmtcolor}{rgb}{0,0,0} %color of comments, black
%-------------------------------------------------------------------
\newcommand{\paraSpc} {\hspace*{\fill} \setlength{\parskip}{-2pt}} % reduce space between paras
%-------------------------------------------------------------------
\newcommand{\itemSpc} {\setlength{\itemsep}{-0pt}} % reduce space between para items
%-------------------------------------------------------------------
% Special commands for MACHINE
%-------------------------------------------------------------------
\newcommand{\MACHINE}[1] { \item[\textcolor{keycolor}{MACHINE } #1] \paraSpc }
\newcommand{\REFINES}[1]{ \item[\textcolor{keycolor}{REFINES }] #1 \paraSpc }
\newcommand{\SEES}[1]{ \item[\textcolor{keycolor}{SEES }] #1 \paraSpc }
\newcommand{\VARIABLES}{\item[\textcolor{keycolor}{VARIABLES}] \paraSpc }
\newcommand{\INVARIANTS}{ \item[\textcolor{keycolor}{INVARIANTS}] \paraSpc }
\newcommand{\VARIANT}{ \item[\textcolor{keycolor}{VARIANT}] \paraSpc }
\newcommand{\EVENTS}{ \item[\textcolor{keycolor}{EVENTS}] \paraSpc }
\newcommand{\INITIALISATION}{ \item[\textcolor{keycolor}{Initialisation}] \paraSpc }
\newcommand{\EVT}[1]{ \item[\textcolor{keycolor}{Event} \textit{#1} $\defi$ ] \paraSpc } % opt1
% Option: deactivate above command and reactivate
% the command below to display only event name
%\newcommand{\EVT}[1]{ \item[\textit{#1}] $\defi$ \paraSpc } % opt2
\newcommand{\REF}[1]{ \item[\textcolor{keycolor}{refines}] \textit{#1} \paraSpc }
\newcommand{\EXTD}[1]{ \item[\textcolor{keycolor}{extends}] \textit{#1} \paraSpc }
\newcommand{\Status}[1]{ \item[\textcolor{keycolor}{Status}] #1 \paraSpc }
\newcommand{\AnyPrm}{ \item[\textcolor{keycolor}{any}] \paraSpc \itemSpc }
\newcommand{\WhereGrd}{ \item[\textcolor{keycolor}{where}] \paraSpc \itemSpc }
\newcommand{\WhenGrd}{ \item[\textcolor{keycolor}{when}] \paraSpc \itemSpc }
\newcommand{\Witnesses}{ \item[\textcolor{keycolor}{with}] \paraSpc \itemSpc }
\newcommand{\ThenAct}{ \item[\textcolor{keycolor}{then}] \paraSpc \itemSpc }
\newcommand{\BeginAct}{ \item[\textcolor{keycolor}{begin}] \paraSpc \itemSpc }
\newcommand{\EndAct}{ \item[\textcolor{keycolor}{end}] \paraSpc }
%-------------------------------------------------------------------
% Special commands for CONTEXT
%-------------------------------------------------------------------
\newcommand{\CONTEXT}[1]{ \item[\textcolor{keycolor}{CONTEXT }] #1 \paraSpc }
\newcommand{\EXTENDS}[1]{ \item[\textcolor{keycolor}{EXTENDS }] #1 \paraSpc }
\newcommand{\SETS}{ \item[\textcolor{keycolor}{SETS}] \paraSpc }
\newcommand{\CONSTANTS}{ \item[\textcolor{keycolor}{CONSTANTS}] \paraSpc }
\newcommand{\THEOREMS}{ \item[\textcolor{keycolor}{THEOREMS}] \paraSpc }
\newcommand{\AXIOMS}{ \item[\textcolor{keycolor}{AXIOMS}] \paraSpc }
%-------------------------------------------------------------------
% General commands used in both machines and contexts
%-------------------------------------------------------------------
% Specification Title
\newcommand{\BTitle}[3]{
\item[\fbox{\parbox{6in}{\centering{~\\An Event-B Specification of #1
\\Creation Date: #2 @ #3\\}}}]
}
% End of MACHINE or CONTEXT
\newcommand{\END}{ \item[\textcolor{keycolor}{END}] \hspace*{\fill} }
% Printing non-labelled elements
% (i.e. variables, sets and constants)
% \newcommand{\Item}[1]{ \item[\textcolor{codecolor}{$\tt#1$}] \itemSpc }
\newcommand{\Item}[1]{$\tt#1$ \itemSpc }
\newcommand{\ItemX}[1]{ $\it#1$ \itemSpc }
% Printing an element with label name
% (i.e. invariants, theorems, axioms, witnesses and actions)
% parameter #1 is a label name and #2 is its content
\newcommand{\nItem}[2]{ $\tt #1:$ $\tt #2$ \itemSpc } % opt1
\newcommand{\nItemX}[2]{ $\tt #1: \it #2$ \itemSpc } % opt1
% Below is an alternative command for printing with no label
%\newcommand{\nItem}[2]{ \item[] $#2$} % opt2
% Commentations, reselect the second option for displaying asterisks
% - Newline comment
\newcommand{\cmt}[1]{ \hspace*{\fill}\\\textcolor{cmtcolor}{ #1}} %opt1
%\newcommand{\cmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt2
% - Back Comment, for variables, sets and constants
\newcommand{\bcmt}[1]{~~~ \textcolor{cmtcolor}{#1}} %opt1
%\newcommand{\bcmt}[1]{~~~ $/\ast$ #1 $\ast/$} %opt2
% Select opt3 or opt4 (including asterisks) if you want to display this kind of comments
% on the newline like the newline comment
%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ #1} %opt3
%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt4
%-------------------------------------------------------------------
%%
%% This is file `bsymb.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% bsymb.dtx (with options: `package')
%%
%% This is a generated file.
%%
%% Copyright (C) 2004 by Laurent Voisin <laurent.voisin at inf.ethz.ch>
%%
%% This file may be distributed and/or modified under the
%% conditions of the LaTeX Project Public License, either version 1.3
%% of this license or (at your option) any later version.
%% The latest version of this license is in:
%%
%% http://www.latex-project.org/lppl.txt
%%
%% and version 1.3 or later is part of all distributions of LaTeX
%% version 2003/12/01 or later.
%%
\NeedsTeXFormat{LaTeX2e}[1999/06/01]
\ProvidesPackage{bsymb}
[2005/04/27 v1.5 Symbols for the B language]
\RequirePackageWithOptions{amssymb}
\newcommand\bsymb@defop[2]{
\newcommand{#1}{\mathop{#2}\nolimits}
}
\newcommand\bsymb@deford[2]{
\newcommand{#1}{\mathord{#2}}
}
\bsymb@deford{\bfalse}{\bot}
\bsymb@deford{\btrue}{\top}
\newcommand{\limp}{\mathbin\Rightarrow}
\newcommand{\leqv}{\mathbin\Leftrightarrow}
\bsymb@deford{\qdot}{\mkern1mu\cdot\mkern1mu}
\newcommand\defi{\mathrel{\widehat=}}
\bsymb@defop{\pow}{\mathbb P\hbox{}}
\bsymb@defop{\pown}{\mathbb P_1}
\newcommand{\cprod}{\mathbin\times}
\newcommand{\bunion}{\mathbin{\mkern1mu\cup\mkern1mu}}
\newcommand{\binter}{\mathbin{\mkern1mu\cap\mkern1mu}}
\bsymb@defop{\union}{\mathrm{union}}
\bsymb@defop{\inter}{\mathrm{inter}}
\newcommand{\Union}{\bigcup\nolimits}
\newcommand{\Inter}{\bigcap\nolimits}
\renewcommand{\emptyset}{\mathord\varnothing}
\newcommand{\rel}{\mathbin\leftrightarrow}
\newcommand{\trel}{\mathbin{\leftarrow\mkern-14mu\leftrightarrow}}
\newcommand{\srel}{\mathbin{\leftrightarrow\mkern-14mu\rightarrow}}
\newcommand{\strel}{\mathbin{\leftrightarrow\mkern-14mu\leftrightarrow}}
\bsymb@defop{\dom}{\mathrm{dom}}
\bsymb@defop{\ran}{\mathrm{ran}}
\newcommand{\fcomp}{\mathbin;}
\newcommand{\bcomp}{\circ}
\bsymb@defop{\id}{\mathrm{id}}
\newcommand{\domres}{\mathbin\lhd}
\newcommand{\domsub}{\mathbin{\lhd\mkern-14mu-}}
\newcommand{\ranres}{\mathbin\rhd}
\newcommand{\ransub}{\mathbin{\rhd\mkern-14mu-}}
\newcommand{\ovl}{\mathbin{\lhd\mkern-9mu-}}
\newcommand{\dprod}{\mathbin\otimes}
\bsymb@defop{\prjone}{\mathrm{prj}_1}
\bsymb@defop{\prjtwo}{\mathrm{prj}_2}
\newcommand{\pprod}{\mathbin\|}
\newcommand{\bsymb@partial}[2]{
\mathbin{\mkern#2mu\mapstochar\mkern-#2mu#1}
}
\newcommand{\pfun}{\bsymb@partial\rightarrow6}
\newcommand{\tfun}{\mathbin\rightarrow}
\newcommand{\pinj}{\bsymb@partial\rightarrowtail9}
\newcommand{\tinj}{\mathbin\rightarrowtail}
\newcommand{\psur}{\bsymb@partial\twoheadrightarrow6}
\newcommand{\tsur}{\mathbin\twoheadrightarrow}
\newcommand{\tbij}{\mathbin{
\rightarrowtail
\mkern-18mu\twoheadrightarrow}
}
\bsymb@defop{\fin}{\mathbb F\hbox{}}
\bsymb@defop{\finn}{\mathbb F_1}
\bsymb@deford{\nat}{\mathbb N}
\bsymb@deford{\natn}{\mathbb N_1}
\bsymb@deford{\intg}{\mathbb Z}
\bsymb@defop{\card}{\mathrm{card}}
\newcommand{\upto}{\mathbin{.\mkern1mu.}}
\bsymb@defop{\upred}{\mathrm{pred}}
\bsymb@defop{\usucc}{\mathrm{succ}}
\newcommand\expn{\mathbin{\widehat{\enskip}}}
\bsymb@deford{\Bool}{\mathrm{BOOL}}
\bsymb@deford{\True}{\mathrm{TRUE}}
\bsymb@deford{\False}{\mathrm{FALSE}}
\bsymb@defop{\bool}{\mathrm{bool}}
\newcommand{\bcmeq}{\mathrel{:\mkern1mu=}}
\newcommand{\bcmin}{\mathrel{:\mkern1mu\in}}
\newcommand{\bcmsuch}{\mathrel{:\mkern1mu\mid}}
\endinput
%%
%% End of file `bsymb.sty'.
\chapter{Reference}
\section{Arithmetic}
\label{arithmetic}
\section{Eclipse}
\label{eclipse}
... Eclipse Definition ...
\section{Event-B}
\label{event-b}
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.
\paragraph{See Also:}
\begin{itemize}
\item \url{http://www.event-b.org}
\end{itemize}
\section{First Order Predicate Calculus}
\label{first_order_predicate_calculus}
\section{Formal Method}
\label{formal_method}
\section{IDE}
\label{ide}
... IDE Definition ...
\section{Naming Convention}
\label{naming_convention}
In this section we describe a recommended naming convention. Good naming conventions save time -- and nerves.
\section{Refinement}
\label{refinement}
... Refinement Definition ...
\subsection{Horizontal Refinement}
\label{horizontal_refinement}
\subsection{Vertical Refinement}
\label{vertical_refinement}
\subsection{Data Refinement}
\label{data_refinement}
\paragraph*{See also:}
\begin{itemize}
\item Data refinement in the trafficlight tutorial (\ref{tutorial_tl_data_refinement})
\end{itemize}
\section{Propositional Calculus}
\label{propositional_calculus}
\section{Rodin}
\label{rodin}
... Rodin Definition ...
\section{Rodin Platform}
\label{rodin_platform}
... Rodin Platform Definition ...
\section{Set Theory}
\label{set_theory}
... Set Theory Definition ...
\documentclass{book}
\usepackage{hyperref}
\usepackage{graphicx}
\usepackage{bsymb}
\usepackage{b2latex}
\usepackage{fancyhdr,lastpage,color}
\def\doculist#1#2{
\vspace{3mm}
\noindent
\begin{tabular}{lp{0.85\textwidth}}
\includegraphics[width=10mm]{#2} & \vspace{-10mm}#1\\
\end{tabular}
}
\def\tick#1{\doculist{#1}{img/tick_64.png}}
\def\info#1{\doculist{#1}{img/info_64.png}}
\def\warning#1{\doculist{#1}{img/warning_64.png}}
\def\pencil#1{\doculist{\vspace{-5mm}#1}{img/pencil_64.png}}
\title{Rodin User Manual v.2.1.1}
\author{Sample of \LaTeX-based Documentation Overhaul\\ \\
Contact Info: Michael Jastram \href{mailto:michael.jastram@formalmind.com}{michael.jastram@formalmind.com}}
\begin{document}
\maketitle
\section*{Introduction}
The Rodin (\ref{rodin_platform}) documentation needs improvement. This has been established at the Deyploy Exec Meeting in 2010. We've been collecting background information and the requirements in the \href{http://wiki.event-b.org/index.php/User_Documentation_Overhaul}{Rodin Wiki}.
We are currently investigating various approaches to managing the documentation. The approach shown here will work as follows:
\begin{itemize}
\item The documentation is kept as \LaTeX.
\item We keep the source in Subversion. That way anybody with access to Subversion can contribute.
\item By keeping the documentation in Subversion, we can keep Rodin and its documentation in sync.
\item We use \href{http://plastex.sourceforge.net/}{plasTeX} to generate HTML and Eclipse Help from the \LaTeX. plasTeX supports templates, so we can use different templates for the two versions (for instance, we would not generate navigation elements for Eclipse Help, as Eclipse Help itself provides navigation).
\end{itemize}
This document demonstrates this approach with a very small portion of the existing Rodin documentation. Obviously, it is just a proof of concept.
\section*{Conventions}
We use the following conventions in this manual:
\tick{Checklists and Milestones are designated with tick.}
\info{Usegful information and tricks are designated by the information sign.}
\warning{Potential problems and warnings are designated by a warning sign.}
\pencil{\begin{description} \item Examples and Code are designated by a pencil.\end{description}}
The Rodin (\ref{rodin_platform}) documentation needs improvement. This has been established at the Deyploy Exec Meeting in 2010. We've been collecting background information and the requirements in the \href{http://wiki.event-b.org/index.php/User_Documentation_Overhaul}{Rodin Wiki}.
\input{tutorial}
\input{reference}
\input{faq}
\end{document}
\chapter{Tutorial}
\label{tutorial}
This tutorial should provide the user with a tour through the most important functionalities of RODIN, so that he gets a understanding of how the program works.
The tutorial doesn't contain all the knowledge that you require. Instead, it touches upon every concept - from installation to set theory to modeling and refinement - and helps you to find gaps in your knowledge.
Before we build a first model, we will cover some basic math.
\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}
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.eclipse.ant.AntLaunchConfigurationType">
<booleanAttribute key="org.eclipse.ant.ui.DEFAULT_VM_INSTALL" value="true"/>
<stringAttribute key="org.eclipse.debug.core.ATTR_REFRESH_SCOPE" value="${working_set:&lt;?xml version=&quot;1.0&quot; encoding=&quot;UTF-8&quot;?&gt;&#10;&lt;resources&gt;&#10;&lt;item path=&quot;/org.rodinp.help.feature&quot; type=&quot;4&quot;/&gt;&#10;&lt;/resources&gt;}"/>
<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_PATHS">
<listEntry value="/org.rodinp.handbook.feature/build.xml"/>
</listAttribute>
<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_TYPES">
<listEntry value="1"/>
</listAttribute>
<listAttribute key="org.eclipse.debug.ui.favoriteGroups">
<listEntry value="org.eclipse.ui.externaltools.launchGroup"/>
</listAttribute>
<stringAttribute key="org.eclipse.jdt.launching.CLASSPATH_PROVIDER" value="org.eclipse.ant.ui.AntClasspathProvider"/>
<stringAttribute key="org.eclipse.jdt.launching.JRE_CONTAINER" value="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/java-6-openjdk"/>
<stringAttribute key="org.eclipse.jdt.launching.MAIN_TYPE" value="org.eclipse.ant.internal.launching.remote.InternalAntRunner"/>
<stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="org.rodinp.handbook.feature"/>
<stringAttribute key="org.eclipse.jdt.launching.SOURCE_PATH_PROVIDER" value="org.eclipse.ant.ui.AntClasspathProvider"/>
<stringAttribute key="org.eclipse.ui.externaltools.ATTR_LAUNCH_CONFIGURATION_BUILD_SCOPE" value="${none}"/>
<stringAttribute key="org.eclipse.ui.externaltools.ATTR_LOCATION" value="${workspace_loc:/org.rodinp.handbook.feature/build.xml}"/>
<stringAttribute key="process_factory_id" value="org.eclipse.ant.ui.remoteAntProcessFactory"/>
</launchConfiguration>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.rodinp.handbook</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.pde.ManifestBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.SchemaBuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.pde.PluginNature</nature>
</natures>
</projectDescription>
bin.includes = plugin.xml,\
*.xml,\
*.html,\
icons/,\
images/,\
styles/
<?xml version='1.0' encoding='ISO-8859-1' ?>
<plugin
id="org.rodinp.handbook"
name="Rodin Handbook v.2.1.1"
version="1.0.0.qualifier"
provider-name="Formal Mind GmbH (formalmind.com)">
<extension point="org.eclipse.help.toc">
<toc primary="true" file="eclipse-toc.xml" />
</extension>
</plugin>
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment