% thesis-front.tex --- thesis front matter -*-latex-*-

% Copyright (C) 2020 Amin Bandali <bandali@uwaterloo.ca>

% This file is part of Amin Bandali's MMath thesis.

% This thesis is free software: you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation, either version 3 of the License, or
% (at your option) any later version.

% This thesis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this thesis.  If not, see <https://www.gnu.org/licenses/>.


%% ===================================================================
%% Title page
%% ===================================================================

%% suppress page number and any headers or footers
\pagestyle{empty}
\pagenumbering{roman}

\begin{titlepage}
  \begin{center}
    \vspace*{1.0cm}

    \LARGE A Comprehensive Study of\\
    \Huge Declarative Modelling Languages

    \vspace*{1.0cm}

    \normalsize
    by\\

    \vspace*{0.8cm}

    \LARGE
    \textsc{\addfontfeature{Letters=UppercaseSmallCaps,%
        LetterSpace=6.0}\name}\\

    \vspace*{2.8cm}

    \normalsize
    A thesis\\
    presented to the University of Waterloo\\
    in fulfillment of the\\
    thesis requirement for the degree of\\
    Master of Mathematics\\
    in\\
    Computer Science\\

    \vspace*{1.8cm}

    Waterloo, Ontario, Canada, 2020\\

    \vspace*{0.8cm}

    \raisebox{-0.05em}{\small\copyright} \
    \textsc{\addfontfeature{Letters=UppercaseSmallCaps,
        LetterSpace=6.0}\name{} 2020}
  \end{center}
\end{titlepage}

%% rest of the front pages should be numbered using Roman numerals
%% starting with `ii', and contain no headers
\pagestyle{plain}
\setcounter{page}{2}

%% ends the current page and causes all figures and
%% tables that have so far appeared in the input to be
%% printed; and in a two-sided printing style, it also
%% makes the next page a right-hand (odd-numbered)
%% page, producing a blank page if necessary
\cleardoublepage

%% ===================================================================
%% Author's Declaration
%% ===================================================================

\begin{center}\textbf{Author's Declaration}\end{center}

\noindent
I hereby declare that I am the sole author of this thesis.  This is a
true copy of the thesis, including any required final revisions, as
accepted by my examiners.

\bigskip

\noindent
I understand that my thesis may be made electronically available to
the public.

\cleardoublepage

%% ===================================================================
%% Abstract
%% ===================================================================

\begin{center}\textbf{Abstract}\end{center}

Declarative behavioural modelling is a powerful modelling paradigm
that enables users to model system functionality abstractly and
formally.  An abstract model is a concise and compact representation
of key characteristics of a system, and enables the stakeholders to
reason about the correctness of the system in the early stages of
development.

There are many different declarative languages and they have greatly
varying constructs for representing a transition system, and they
sometimes differ in rather subtle ways.  In this thesis, we compare
seven formal declarative modelling languages \B, \eventb, \alloy,
\dash, \tla, \pluscal, and \asmetal{} on several criteria.  We
classify these criteria under three main categories: structuring
transition systems (control modelling), data descriptions in
transition systems (data modelling), and modularity aspects of
modelling.  We developed this comparison by completing a set of case
studies across the data- vs. control-oriented spectrum in all of the
above languages.

Structurally, a transition system is comprised of a snapshot
declaration and snapshot space, initialization, and a transition
relation, which is potentially composed of individual transitions.  We
meticulously outline the differences between the languages with
respect to how the modeller would express each of the above components
of a transition system in each language, and include discussions
regarding stuttering and inconsistencies in the transition relation.
Data-related aspects of a formal model include use of basic and
composite datatypes, well-formedness and typechecking, and separation
of name spaces with respect to global and local variables.  Modularity
criteria includes subtransition systems and data decomposition.  We
employ a series of small and concise exemplars we have devised to
highlight these differences in each language.  To help modellers
answer the important question of which declarative modelling language
may be most suited for modelling their system, we present
recommendations based on our observations about the differentiating
characteristics of each of these languages.

\cleardoublepage

%% ===================================================================
%% Acknowledgements
%% ===================================================================

\begin{center}\textbf{Acknowledgements}\end{center}

I would like to thank my supervisor Dr. Nancy A. Day, for her
continued support throughout my Master's studies, and for teaching me
so many valuable lessons, including how to do research and how to
write about it.  Her vast knowledge and kindness, and her supporting
me as I worked my way through different research topics and learned
new things has been paramount in me arriving at where I am today.  I
will always be thankful to her, for I have bettered not just as a
researcher but as a person as well.

I sincerely thank Dr. Joanne M. Atlee and Dr. Derek Rayside, for their
agreeing to read my thesis and provide insightful comments in an
incredibly short period of time, due to the my life circumstances.

I would like to thank my colleagues Ali Abbassi, Jose Serna, Khadija
Tariq, Elias Eid, Tamjid Hossain, and Joseph Poremba for our fruitful
discussions and collaborations as a research group.

I would also like to thank all of my teachers and mentors who, one way
or another, have had a role in helping me get to where I am today.  As
such, I thank my wonderful Computer Science teachers including
Mr. Farzaneh and Mr. Seniuk throughout grade school and high school
for inspiring me and encouraging me to always explore and learn more.

I would like to thank Dr. Jonathan S. Ostroff for introducing me to
formal methods, and teaching me so much about it and its important
role in software engineering for building reliable and correct
systems.  I also thank my mentor and good friend Simon Hudon who I
always look up to, for teaching me about formal logic and formal
methods along with Dr. Ostroff, and for our countless fruitful
discussions.  Who would have thought a simple email about the formal
specification of a binary search implementation would lead us to learn
about our mutual interest in Haskell, and be the start of many more
discussions, conversations, and our friendship!

I would like to thank Dr. Richard M. Stallman (rms) for launching the
GNU Project and the Free Software movement, founding the Free Software
Foundation, and dedicating his life to giving the gift of computing
freedom to people all around the world.  I am inspired by rms and the
many other folks who help the cause of the free software movement, by
either directly working on free software or contributing through
various other means, to give a hand in building a world where we the
people can carry out our computations in freedom.

Finally, I would like to thank my family and friends for their love
and support throughout my life.  I~am forever grateful to my parents
and grandparents for their unconditional love and guidance they gave
me in all stages of my life, and for their immense sacrifices in order
to provide an opportunity for my brother and I to build ourselves a
better future.

\cleardoublepage

%% ===================================================================
%% Dedication
%% ===================================================================

\begin{tabular}{p{0.5\textwidth} p{0.5\textwidth}}
  \vspace{0pt} \begin{tabular}[c]{@{}c@{}}
    To my loving mother Roya,\\
    my guiding father Bardia,\\
    my dear brother Hossein,\\
    my beloved grandparents\\
    Ali, Ziba, Feizalah, and Farangis,\\
    and my late teachers\\
    Hasan Jalili,\\
    Mahin Mohammadiyoun,\\
    and Aliasghar Yousefinia
  \end{tabular} &
  \vspace{0.23em} \includegraphics{thesis-dedication-fa}
\end{tabular}

\cleardoublepage

%% ===================================================================
%% Table of Contents
%% ===================================================================

\renewcommand\contentsname{Table of Contents}
\tableofcontents
\cleardoublepage
\phantomsection          % allows hyperref to link to the correct page

%% ===================================================================
%% List of Table
%% ===================================================================

\addcontentsline{toc}{chapter}{List of Tables}
\listoftables
\cleardoublepage
\phantomsection

%% ===================================================================
%% List of Figures
%% ===================================================================

\addcontentsline{toc}{chapter}{List of Figures}
\listoffigures
\cleardoublepage
\phantomsection

%% change page numbering back to Arabic numerals
\pagenumbering{arabic}


%% Local Variables:
%% tex-main-file: "./bandali-mmath-thesis.tex"
%% End:
