Development process

[reggio@disi.unige.it]

Dear Colleagues,

working to prepare the CFI Notes in Genova we have found several big
connections with methodological problems, so I have put together the
various points and I am sending to be circulate to the methodology
list to start a discussion on such topics.
  Kind regards

     Gianna

========

\documentstyle[12pt]{article}
%
% Sizes for 'large 12 pt'
%
\setlength{\textwidth}{16.0cm}
\setlength{\textheight}{23.0cm}
\hoffset -1.5cm
\voffset -2.25cm

\title{  }
\author{ }

\date{}
\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Development process}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We assume a development process supported by CFI schematically
presented as follows:
\begin{description}
%
\item[Initial requirements]
The essential properties of the system to be developed are determined
and formally defined by a ``loose'' specification
(i.e. a specification admitting a class of
possibly non-isomorphic models).
Each model is a formal abstract
representation of a possible acceptable realization of the system and
vice versa
(i.e. any possible acceptable realization of the system must
be representable by a model of the specification).
%
\item[Refinement of the requirements]
In several steps the initial requirements are refined by making
particular choices about
points not already fixed and by designing parts of the system in a way
to have the required properties.
Each of these steps is formally
represented by a loose specification, whose models
correspond to the possible realizations of the system embodying the
choices done until that step.
%
\item[Final design]
After a finite number of steps all open points have been fixed and all
parts of the systems have been designed.
This step is formally represented by a
``design specification''
i.e. a specification having 1 (up to isomorphism) model:
the formal abstract representation of the developed system.

(We know that some people, for example Kreowski, does not like the above
definition of design and perhaps something related to design is missing.
We would consider further this point.)
%
\item[Interface (perhaps waiting for a better name)]
Loosely speaking the ``connection''
between the parts of the system abstractly and formally described
in the design specification
and the final implementation.
%
\item[Implementation]
A program in some EXISTING programming language realizing\slash
implementing the system formally
 abstractly represented by the model given at the previous step.
\end{description}

>From what said above it should be clear the distinction between:
\begin{description}
\item[loose or better requirement specification:]  many models
\item[design specification]: 1 model (?)
\item[program]: corresponding to 1 model
\end{description}

As an example consider:
\begin{itemize}
\item
first-order many sorted specifications (class of non-isomorphic
algebras)
\item
conditional many-sorted specifications with initial semantics
(1 up to isomorphism algebra)
\item
Pascal programs, where the operations of the algebras are in
correspondence
with Pascal functions using in their bodies imperative constructs as
assignments
and while's.
\end{itemize}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Role of initial specifications}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
We assume  that the CFI should support also a kind of specifications
determining exactly 1 adt
(to be used in the last step of the specification phase, when a
detailed design
of the system is abstractly and formally presented).
Initiality is a tool very well suited to define this kind of
specifications,
and the restrictions that we have to impose on specifications to make
the initiality constraint sensible (e.g. only conditional axioms) are
methodologically
consistent with the idea of defining the design of a system.

In order to understand why initiality could be useful, let us
outline some methodological guidelines showing how initiality
could be used in practice.

After some years of exeprience,
we have drawn the following methodological guidelines for
writing an algebraic specification with initial semantics:
%
\begin{itemize}
%
\item
Determine the sort of interest (main sort)
%
\item
Determine and specify, if any, the auxiliary adts
(subparts, observations of the main values)
%
\item
Determine the constructors for the elements of the main sort
(i.e. a set of operations such that any element of the main sort may be
represented
by a combination of such operations  possibly using elements of the
auxiliary adts)
%
\item (*)
Determine the properties of such constructors and express them by means
of conditional axioms (such axioms express
that under some conditions the same element may be represented by
different combinations of constructors)
%
\item
Determine the operations and the predicates acting on the elements of
the main sort
%
\item
Define the above operations and predicates by means of
conditional axioms; there should be at least an axiom for each of them
and
each constructor and the result of the operations should always be
expressible by a combination of constructors
\end{itemize}

Very frequently the step (*) is null, i.e. no
identifications on the constructors.
In such cases it may be possible to replace the
specification with the initial constraints with a simpler and
direct definition
of the resulting algebra following, e.g., a ML-like functional style.
However, when (*) is not null (e.g. in the specifications of sets,
multisets,...) to replace the initial constraint usually
results in a kind
of implementation and not in an abstract specification (think of the
definition of sets in ML).


%%%
\section{About behavioural}
%%%

\subsection{Loose specifications}

By behavioural encapsulation we mean:
\begin{quote}
given a specification S with a class of models M and
 a set of formulae OBS on a  signature common to all models in M,
{\em behaviour S w.r.t OBS},
is the specification whose class of models is
\\
\{ A $\mid$ there exists B$\in$ M s.t. for all $\phi\in$OBS
A$\models\phi$
iff B$\models\phi$\}
\end{quote}

Perhaps here we are missing the point and  are open to motivations
changing our view, but from our experience, we tend to behave that
behavioural encapsulation should not be included in the CFI since:
\begin{itemize}
\item
We conjecture that
a specification using the behavioural encapsulation constraint
may be replaced by an equivalent one using a more powerful logic
(e.g. behavioural encapsulation on a conditional specification may be
replaced by a first order specification).
In practice this works also, surprisingly, in the case of reactive\slash
concurrent systems.
(Any theoretical result supporting this conjecture ?)
\item
>From a methodological point of view we think that the equivalent
specification in  a more powerful logic is more readable and
easier to write, since the properties of
the resulting system are expressed explicitly and directly.
\end{itemize}

%
\subsection{Behavioural model}
%
Especially in the case of the specification of reactive\slash
concurrent systems,
we have found useful the constraint that we call ``behavioural
model'' intended as follows:
\begin{quote}
given a specification S with a class of models M
and a set of ``experiments (formulae with a hole)'' EXP on a
signature common to all models in M,
the {\em behaviour model of  S w.r.t OBS\/}
is the algebra A characterized by
A $\models$ t= t'  iff for all e$\in$EXP, for all B$\in$ M,

 B$\models$ e[t] iff  B$\models$ e[t']
\end{quote}
This setting may be further extended to consider ``bisimilar
experiments'' (see ....).

Under some conditions the above definition determines
1 (up to isomorphism) model of the given specification.


 \end{document}




===================================================================

Gianna Reggio
Dipartimento di Informatica e Scienze dell'Informazione
Universita' di Genova
Via Dodecaneso 35 - 16146 Genova (Italy)
Phone: +39-10 3536702
Fax: +39-10 3536699
email: reggio @ disi.unige.it