Development Process

[reggio@disi.unige.it]

Dear Collegues,
unfortunately, due to some technical problems in August I was not on
Methodology list so I had never received the Andrezj-Don message about
development process; now I have got a copy of it (thanks to the nice
archives of the mailing lists in Aarhus), and attached there are
further considerations on the subject (as a complete Latex document).

  Best 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{Development process - 2}
\author{Egidio Astesiano - Gianna Reggio}

\date{}
\begin{document}
\maketitle

Here there is a brief revised version of our  idea of development process
(devised starting from earlier work from Sannella-Tarlecki-Wirsing).

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[Development step]
The system is developed in several steps; each step correspond
to\slash consists of
\begin{itemize}
\item {\em refinement\/}, i.e. when
the requirements  given in the previous step (about parts of the system)
are refined by making
particular choices about open points;
\item {\em realization\/},
i.e. when parts of the system are realized in such a way
to satisfy the  properties required in the previous specification.
\end{itemize}
Notice that a development step may be a refinement for some parts and a
realization for some other parts, also if it is better to keep each
step enough simple.

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.

Clearly there is a notion of ``correctness'' of a step
(implementation notion between specifications):

if SP1 and SP2 are respectively
the specifications given at steps i and step i+1,
then SP2 is implemented by SP1 via alpha for an ``appropriate'' alpha

where

SP2 is implemented by SP1 via alpha iff

alpha is a function from specifications to specifications s.t.

Mod(alpha(SP2)) are contained in  Mod(SP1)

alpha represents the ``realization component'', i.e it says how the parts
of SP1
are realized out of those of SP2; while the inclusion of the model classes
ensures that all requirements of SP1 are satisfied (refinement component).
%
\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 should consider further this point.)

Notice that, very frequently, a development step
is formalized  by what we call a {\em mixed-specification\/}
(i.e. a specification defined by  freely combining  design
subspecifications  [to represent the realized parts] and
loose specifications [to represent the parts for which only some
properties have been given]);
mixed-specifications are needed since during the development
some parts may be fully designed when for other ones there are just some
requirements.
%
\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 (perhpas modulo isomorphism)
\item[program]: running code implementing the design specification
in a current programming language.
\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}

%%%%%%%%%%%%%
\subsection{Relationships with the Andrezj-Don proposal}
%%%%%%%%%%%%%

In our opinion there are three, almost orthogonal,
points in which the two proposals differ:

meaning of programs  (the most relevant point);

use of functional specifications\slash modules;

which part of the whole is ``designed\slash realized''
in each step of the development process.


%%%%%
\paragraph{Meaning of programs}
%%%%%

First of all we think we need
to clarify some terminology, perhaps to be used as standard in the CFI.

What is the meaning of ``program, programming language'' ?

\begin{description}
\item[1]
Programming language =
 some EXISTING, well-known, non-accademic .... programming language, e.g. C,
 PASCAL, ADA, .....

A program is then the ``thing'' to be effectively run on a computer at the end
of the development.
%
\item[2]
Programming language =
a (specification) language for presenting 1 model belonging
to the class (or to a particular subclass)
of the models for  (the chosen variant of) CFI,
whose  features are ``enough abstract\slash near to the model''.

In some sense  it may be a specification
language  for the definition of (design) specifications following
a model oriented approach instead of
the axiomatic one proper of algebraic specifications.
Examples of ``programming languages''
intended in this sense  are: ML, something inside the OBSCURE approach,
in the concurrency field two nice
cases are the Milner's CCS and the Hoare's CSP.
\end{description}

Sometimes the programs of  languages of  kind 2 may be interpretable
and so we can have a way to run them, but usually this
is not based on the standard efficient techniques proper of the field
(e.g.  the run of a CCS behaviour is the generation of a labelled tree).
This should instead be considered as a case of
``rapid prototyping of  specifications''.

We know that in several cases,  languages of  kind 2 could be extremely nice
when considered as programming languages in the sense of 1 forgetting
efficiency
(we think that the realm of ML is the Heaven of programmers);
but for a good acceptance of the results of our common efforts we have to
consider:
\begin{itemize}
\item
it is already hard to get acceptance of formal
specification methods which are based on concepts\slash notations
 non-familiar to the users,
\item
some of the most successful formal methods are those enough near to the usual
programming languages concepts
(see e.g. UNITY, B), or having ``familiar parts'' (e.g. LARCH);
\end{itemize}
and so  let the user have their favorite stuff at least at the end of
the development process.


In what follows we will use  the words
``design specification'' where
Andrzej-Don uses ``program'', but everything could be rephrased
using program in an almost orthogonal way.


%%%%%
\paragraph{The parameterization point}
%%%%%

>From what we have understood
the parametric specifications of the Andrzej-Don's approach play the same
role of our mixed-specifications;
they are the tool for giving the specification of a system at an intermediate
step of development, where some parts are completely determined
(defined by a design specification) while for others we have only some
properties
(defined by a requirement specification).

>From a specification language point of view, to take care of
mixed-specifications means to have:
\begin{itemize}
\item
two different kinds of basic specifications: design
(e.g. algebraic  specifications with initial semantics and\slash or
model-oriented specifications) and
requirement (e.g. algebraic specifications with loose semantics and\slash or
behavioural semantics);
\item
structuring constructs acting on specifications
without worrying about their kinds
(e.g
\begin{verbatim}
MIX-SP1 =
requirement
use DESIGN-SP
......

MIX-SP2 =
design
use REQUIREMENT-SP
......

MIX-SP3 =
design
use REQUIREMENT-SP, DESIGN-SP
......
\end{verbatim}
Parametric specifications (non-higher order) may be present but just for
the case of
parameterized systems and for reusing (e.g. a parametric specification of LIST)
\end{itemize}

We conjecture that the two approaches are equivalent iff on the
parameterized side
we have the full machinery, including parameterized specifications
of whatever order (e.g. taking as parameters parametrized specifications).
Notice that the formal semantics of the mixed-specifications relys on some form
of parameterized specifications.

We should now compare two approaches w.r.t their use in practice:
\begin{description}
\item[parametric way]\

It requires some overhead, since in each case one has to give explicitly
the formal parameters  with their properties, the actual ones, ....

It makes explicit\slash very clear
 the distinction between the requirement (to be developed)
 and the design (already developed) parts \verb#:)#.

By restricting the allowed forms of  parameterizations, we can  impose a
discipline on the development in a simple way.
%
\item[mixed-specifications]\

No overheads, neither in the resulting specifications nor in the
specification language.
The functional overhead is hidden inside the specification language,
it will appear when giving its semantics.

One needs only to learn\slash master the structuring constructs for
specifications;
 the distinction between requirement\slash design is in some
sense  ``transparent'' to the user.
In the above examples one do not need to know what
is the kind of \verb#REQUIREMENT-SP# and of  \verb#DESIGN-SP#
to define such mixed-specifications.
On the other hand it may be hard to understand which are the parts
still at the requirement level \verb#:(#

More freedom in the splitting between the design and the requirement parts
at each development step
(e.g. as first step one can give a design of the natural
numbers, since the system to be developed uses them);
we need to discuss whether this freedom is too much.
\end{description}


%%%%%
\paragraph{Which parts of the whole are ``designed\slash realized''
at each step of the development process}
%%%%%

While our proposal leaves the developer free about what to do at each step,
the Andrzej-Don's proposal, put some discipline on it, by
suggesting that at each step,
\begin{itemize}
\item
one has 1 part to be developed, say P, (the parameter),

\item must act on P by

finding out a subpart, say S, to be developed afterwards,

giving its properties (the new parameter)

and
determining\slash designing  how   to build P by using S.
\end{itemize}
This development process seems enough natural and covers a lot of cases
(we have followed it also for several concurrent systems).
The only debatable point is its generality (it corresponds to a kind of
top-down).

We think that this point requires some discussion inside the CFI
methodology group:

For what concerns the activities to be done during a development step:

Should some discipline  be given?

In such case, should we give
\begin{itemize}
\item
just one way ?
\item
several ways (with some hints for choosing them) ?
\item
generic recomendations\slash hints\slash warnings ?
\end{itemize}


 \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