% modularity.tex --- modularity aspects of languages -*-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/>.


\chapter{Modularity}
\label{chp:mod}

To create large models, some form of modularity is needed.  In this
chapter, we discuss how each language provides support for modularity
in a description of a transition system.  Our case studies were not
large enough to exercise the differences presented in this chapter,
and we cannot use small exemplars to showcase these differences in a
meaningful way.  Modularity can be evaluated from two points of view:
\begin{enumerate}[label=(\arabic*),ref=(\arabic*)]
\item \label{itm:mod/decomp-parts} How can a description of a single
  transition relation be decomposed into multiple parts?  This
  decomposition may take the form of
  \begin{enumerate}[label=(\alph*),ref=(\arabic{enumi})(\alph*)]
  \item subtransition systems that are composed to create the single
    top-level transition relation implicitly or explicitly, where a
    subtransition system is a full description of a transition system;
    or
  \item \label{itm:mod/decomp-parts/data} subformulas relevant to
    other aspects of the model \md such as a grouping information
    (axioms, \emph{etc.}) regarding a unit of data \md which we refer
    to as a data decomposition.
  \end{enumerate}
\item \label{itm:mod/decomp-files} How can a description of a single
  transition system be decomposed into multiple files?  Typically a
  decomposition into multiple files involves interfaces that can be
  parameterized and have private and public parts.
\end{enumerate}

It may be possible for the decompositions of
\ref{itm:mod/decomp-parts} to be realized in multiple files.  In the
following, we describe the different means within a language of
decomposing the transition relation (\emph{i.e.},
\ref{itm:mod/decomp-parts} above) and within this discussion address
when/how different parts of the transition relation can be realized in
multiple files.  Both \ref{itm:mod/decomp-parts} and
\ref{itm:mod/decomp-files} may involve differing namespaces.

\begin{table}[htbp]
  \centering
  \caption{Summary of modularity aspects of languages}
  \label{tab:mod/summary}
  \input{table/mod-summary}
  \raggedright
  \footnotesize
  \vspace{0.25em} \textbf{*}: Due to \dash's per-\dashcode{state}
  namespaces.
\end{table}

In \B, the definition of the transition relation is implicit, and it
is possible to decompose a transition system into subtransition
systems.  Each \B{} machine resides in one file, under one namespace.
The \B{} language has extensive constructs for creating relationships
between machines, using the keywords \bcode{SEES}, \bcode{INCLUDES},
\bcode{PROMOTES}, \bcode{EXTENDS}, \bcode{USES}, and
\bcode{IMPORTS}~\cite{b-manref}.  A \B{} machine can reference the
name of another machine along with these keywords to establish the
desired kind of relationship with that machine.  The \bcode{SEES}
keyword grants a machine read-only access to \emph{see} the data
components (\emph{i.e.} sets, constants, and variables) of another
machine, and the \bcode{INCLUDES} keyword grants read-write access to
the data components of the included machine, allowing instantiation if
the machine is parameterized (over a scalar or set parameter).  More
specifically, \bcode{INCLUDES} allows establishing a subtransition
system relationship where the \bcode{SETS}, \bcode{CONSTANTS},
\bcode{PROPERTIES}, \bcode{VARIABLES}, \bcode{INVARIANT},
\bcode{ASSERTIONS}, and \bcode{INITIALISATION} sections of the
included machine are in effect prepended to those of the including
machine.  The details of the remaining keywords and the relationships
they establish are beyond the scope of this work.  There is no support
for syntax overloading in \B.

In \eventb, the definition of the transition relation cannot be
further decomposed into subtransition systems.  In \eventb, there are
two kinds of files: contexts and machines.  Contexts describe
non-changing parts of the system, namely the sets, constants, and
axioms; and a machine contains the snapshot and transitions (the
transitions are implicitly combined to build the transition relation).
A machine can \emph{see} any number of contexts by adding their names
under its \eventbcode{SEES} section.  The only possible relationship
between two machines in a project is where one machine
\eventbcode{REFINES} another.  There is no support for syntax
overloading in \eventb.

An orthogonal perspective on the notion of modularity in \B{} and
\eventb{} is the concept of
\emph{refinement}~\cite{DBLP:books/daglib/0015096,
  DBLP:books/daglib/0024570, b-manref, rodin-handbook}.  The idea
behind refinement is starting the description of a transition system
at a very abstract level and with minimal details, and gradually
refining that description over several refinement steps to arrive at a
more concrete and complete description.  Both \B{} and \eventb{} have
tool support dedicated to assisting the modeller with performing
refinement steps and doing them correctly, by presenting various proof
obligations that need to be proven correct at each step.  Details on
refinement is beyond the scope of this work.

In \alloy, the definition of the transition relation is explicit as a
formula.  Therefore any means in \alloy{} of decomposing formulas can
be used to decompose the description of a transition system.  In
Chapter~\ref{chp:control}, we discussed some typical styles of
decomposing transition systems into different formulas (\emph{e.g.},
with pre and postconditions).  Within one \alloy{} file, the namespace
includes all of the identifiers declared/defined in the current file.

In \alloy, formula decomposition can be split across multiple files.
This decomposition could be for subformulas of the transition system
or for a grouping of axioms regarding a unit of data.  \alloy{} refers
to each file as a module, which may be given a name using the
\alloycode{module} keyword at the beginning of the file.  By default,
all of the identifiers declared or defined in a file are exported,
along with the exported identifiers of all of the other files imported
into the current file using the \alloycode{open} keyword.  However,
signatures, their fields, functions, and predicates can be marked as
\alloycode{private}, making them private to the current module and not
appear in the namespaces of other modules that import the current
module.  To assign a dedicated namespace to the identifiers of an
imported module, we can use \alloycode{open..as}.  For example,
\alloycode{open utils as u} will bring the definitions of the
\alloycode{utils} module into scope under the \alloycode{u} namespace,
and an identifier named \alloycode{test} can be referred to using
\alloycode{u/test}.  In \alloy, a module can be parameterized over an
argument, similar to the notion of genericity in programming
languages.  For instance, \alloy's ordering module is parameterized
over a signature on which the module will impose a linear total order.
In \alloy, for syntax overloading, fields in different signatures can
use the same name, as long as the two signatures do not overlap (by
one being a subset of the other).  In other words, the type signatures
for two fields with the same name must differ at least in the first
column.  Further, two predicates or functions may share the same name,
so long as the type signatures for their arguments are not identical
(\emph{i.e.} an unambiguous name resolution possible).

In \dash, the definition of the state hierarchy for the transition
relation must all reside together in one file because the transition
relation is defined implicitly.  This includes \dash{} invariants
(declared using \dashcode{invariant} or \dashcode{fact}), which must
be in the same file as the transition system.  In \dash, each
\dashcode{state} has a dedicated namespace.  Separate namespaces
create interfaces between states, while still allowing global
communication.  A reference to an identifier in another state must be
given by its fully qualified name.  A qualified name is formed by
following the state hierarchy separating state names with `/' and then
adding the element name.  In \dash, the data modelling aspects of a
transition system are described separately from the state hierarchy
and therefore can be separated into multiple files as in \alloy.
\alloy's file-level module system and namespaces are available to
\dash{} models, with the exception of per-file dedicated namespaces
(using \alloycode{open..as}), which are not yet implemented in \dash.
The details of \alloy's syntax overloading apply to \dash{} as well.

In \tla, the definition of the transition relation is explicit as a
formula.  Therefore any of the means of decomposing formulas in \tla{}
can be used to decompose the description of a transition system.
Within one \tla{} file, the namespace includes all of the identifiers
declared/defined in the current file.

In \tla, formula decomposition can be split across multiple files.
This decomposition could be for subformulas of the transition system
or for a grouping of axioms regarding a unit of data.  \tla{} refers
to each file as a module, which must be given a name using the
\tlacode{MODULE} keyword at the beginning of the file.  By default,
the identifiers of all of the predicates defined in a module are
exported, along with those of the other modules imported into the
current module.  To import another module into the current module, we
use the \tlacode{EXTENDS} keyword.  To import the definitions of a
module \tlacode{M} into a dedicated namespace, instead of importing it
directly, we add a definition \tlacode{M == INSTANCE M}.  We can then
use \tlacode{M!def} to refer to a definition \tlacode{def} from the
\tlacode{M} module.  In \tla, a module is parameterized over its
\tlacode{CONSTANTS}.  As such, if \tlacode{M} has declared
\tlacode{CONSTANTS A, B} (which may potentially be higher-order
operators), they must be instantiated using \tlacode{M == INSTANCE M
  WITH A <- e1, B <- e2}, where \tlacode{e1} and \tlacode{e2} are
\tla{} expressions such as literals or identifiers of sets or
constants from the current namespace.  To mark a definition or an
instantiation as local to the current module, we use the
\tlacode{LOCAL} keyword, preventing it from appearing in the
namespaces of the other modules importing the module.  \tla{} supports
a number of user-definable symbols, but as with other definitions,
they must not clash with any existing definitions for those symbols,
as \tla{} does not support syntax overloading.

In \pluscal, a transition system is defined in an
\pluscalcode{algorithm} block.  The definitions of the transitions
represented using \pluscal{} \pluscalcode{process}es must all reside
together in that \pluscalcode{algorithm} all in one file, because the
transition relation is defined implicitly.  Each \pluscalcode{process}
can optionally have local variables only available to that process,
declared and initialized using the \pluscalcode{variables} keyword
before the beginning of the body of the transition.  Locally-scoped
bindings using \tlacode{LET..IN} \tla{} expressions are possible as
well.  In \pluscal, the data modelling aspects of a transition system
can be described separately from the transition definitions, and
therefore can be separated into multiple files as in \tla.  \tla's
file-level module system is available to \pluscal{} models as well.
The details of \tla's user-definable symbols and lack of syntax
overloading apply to \pluscal{} as well.

In \asmetal, the definition of the transition relation is explicit as
an \asmetal{} \asmcode{rule}.  Therefore any of the means of
decomposing rules in \asmetal{} can be used to decompose the
description of a transition system.  Within one \asmetal{} file, the
namespace includes all of the identifiers declared or defined in the
current file.

In \asmetal, a model can be split across multiple files for
subtransition system and data decomposition.  \asmetal{} refers to
each file as a module, and there are two kinds of modules.  A module
containing a transition system \md \emph{i.e.} a \asmcode{main rule}
(transition relation) and an \asmcode{init} (initial snapshot) section
\md is given a name using the \asmcode{asm} keyword.  Modules not
including the above two constructs can be created using the
\asmcode{module} keyword, and may contain type signatures and
specifications for data units.  A module can selectively export a
subset of its definitions using a comma-separated list of identifiers
with the \asmcode{export} keyword, or export everything at once using
\mbox{\asmcode{export *}}.  To import a module, we use the
\asmcode{import} keyword along with the name of the module, and
optionally a parenthesized comma-separated list of identifiers if only
some of the module's definitions are desired.  \asmetal{} does not
support prefixed/namespaced imports, and there is no support for
parameterized modules.  In \asmetal, functions and transition
definitions may be overloaded, so that functions with different type
signatures can share the same name.

In summary, the \B, \alloy, and \tla, and \asmetal{} languages allow
decomposition of the model into subtransition systems across multiple
files, while \eventb, \dash, and \pluscal{} only allow data
decomposition across multiple files.


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