\section{The Transformation
Functions}\label{transsec}
In this section we shall present the formal semantics we have
given
to a hierarchy
of DFDs.
The more complicated parts will
be illustrated
by means
of small examples. Thus, this section contains a collection
of VDM
functions which transform SA (
with the structure described
in
Appendix A)
to a collection
of VDM modules (represented
in the
structure described
in Appendix B).
\subsubsection{Top level
functions}
The top-level function, which transforms a hierarchy
of data flow
diagrams (an $HDFD$), also takes
as arguments the mini-specifications supplied
by the
user
and the style
in which the composing
operations are
to be generated%
\footnote{The argument
with this information will
be called $style$ thoughout the
definition indicating that it
is the ``style
" (implicit or explicit)
it should
be transformed.}.
\begin{vdm_al}
functions
TransHDFD : HDFD * MSs * (<EXPL>|<IMPL>) ->
set of Module
TransHDFD(hdfd,mss,style) ==
let mainmod=MakeDFDModule(hdfd,mss,style)
in
let mk_(-,-,-,dfdmap,-)=hdfd
in
let mods=
dunion {TransHDFD(dfd,mss,style)
| dfd
in set rng dfdmap}
in
{mainmod}
union mods;
\
end{vdm_al}
For each
module the interface
and the body (the
definitions)
of
the
module must
be created.
\begin{vdm_al}
MakeDFDModule : HDFD * MSs * (<EXPL>|<IMPL>) ->
Module
MakeDFDModule(mk_(dfdid,dss,dfdtopo,dfdmap,dfdsig),
mss,style) ==
let i = MakeInterface(dfdid,dss,dfdtopo,dfdsig,dfdmap),
defs = MakeDefinitions(dfdid,dss,dfdtopo,
dfdsig,mss,style)
in
mk_(ModIdConf(dfdid),i,defs);
\
end{vdm_al}
\noindent The name
of the
module (the first component
of the
returned triple)
is generated
by means
of a configuration function.
Any name ending
in $Conf$ denotes
something which can
be configured
by a user
of a tool translating
DFDs
to VDM.
These configuration
functions should
be defined (
by the user
or by a
tool%
\footnote{Such a tool would obviously also need
to be able
to produce
the abvstract syntax
of strutured analysis
and produce the concrete
syntax
of the VDM specifications which are produced.}
automatically translating DFDs into VDM specifications)
in order
to be able
to
conform
to any specific conventions (e.g.
for naming identifiers) that are used.
At the
end of the formal definition we present an example
of how these
functions can
be defined.
\subsection{Interface
functions}
The interface
of each
module contains an import part
for a
module with the
type information
for all the data stores
and the data flows (only the
types actually used
in the given
module are imported), an import part
for each
of the data transformers that are further decomposed (
and
are described
in their own
module),
and an export part
for the
operation which specifies the functionality
of the given DFD.
\begin{vdm_al}
MakeInterface: DFDId * DSs * DFDTopo * DFDSig * DFDMap ->
Interface
MakeInterface(dfdid,dss,dfdtopo,dfdsig,dfdmap) ==
let tmimp = MakeTypeModImp(dss,
dom dfdtopo),
dfdmimps = MakeDFDModImps(
dom dfdmap,dfdsig),
exp = MakeOpExp(dfdid,dfdsig(dfdid))
in
mk_(({tmimp}
union dfdmimps),exp)
pre dfdid
in set dom dfdsig;
MakeTypeModImp : DSs *
set of FlowId -> Import
MakeTypeModImp(dss,fids) ==
let tysigs= {mk_TypeSig(DSIdConf(dsid))
|dsid
in set dss}
union
{mk_TypeSig(FlowIdTypeConf(fid))
|fid
in set fids}
in
mk_(TypeModConf(),tysigs);
MakeDFDModImps:
set of DFDId * DFDSig ->
set of Import
MakeDFDModImps(dfdids,dfdsig) ==
{mk_(ModIdConf(id),{MakeOpSig(id,dfdsig(id))})
| id
in set dfdids}
pre dfdids
subset dom dfdsig;
MakeOpExp : DFDId * Signature -> Export
MakeOpExp(dfdid,sig) ==
{MakeOpSig(dfdid,sig)};
MakeOpSig : DFDId * Signature -> OpSig
MakeOpSig(dfdid,sig) ==
let opty = MakeOpType(sig),
opst = MakeOpState(sig)
in
mk_OpSig(OpIdConf(dfdid),opty,opst);
MakeOpType : Signature -> OpType
MakeOpType(mk_(il,ol,-)) ==
mk_OpType(MakeType(il),MakeType(ol));
\
end{vdm_al}
In $MakeType$ it can
be seen that multiple flows
to or from a data
transformer are modelled
as product
types.
\begin{vdm_al}
MakeType :
seq of FlowId -> [Type]
MakeType(fidl) ==
cases len fidl:
0 ->
nil ,
1 -> FlowIdTypeConf(
hd fidl),
others -> mk_ProductType([ FlowIdTypeConf(i) | i
in seq fidl])
end;
MakeOpState : Signature ->
seq of Id
MakeOpState(mk_(-,-,sl)) ==
[
let mk_(s,-)=i
in
StateVarConf(s)
|i
in seq sl];
\
end{vdm_al}
\subsection{The main function
for definitions}
The body
of each
module contains a number
of definitions.
The body will contain a
state definition
and if the
DFD contains any data stores, these are included together
with the
data flows between the
system and the external process.
If the DFD contains any data transformers which are
not further decomposed, the body will also contain
definitions for
these. Finally the
module will
always contain a definition
of the
operation which describes the functionality
of that DFD.
\begin{vdm_al}
MakeDefinitions: DFDId * DSs * DFDTopo * DFDSig * MSs *
(<EXPL>|<IMPL>) ->
Definitions
MakeDefinitions(dfdid,dss,dfdtopo,dfdsig,mss,style) ==
let dst = MakeState(dfdid,dss,CollectExtDFs(dfdtopo)),
msdescs = MakeMSDescs(dfdsig,mss),
dfdop = MakeDFDOp(dfdid,dfdtopo,dfdsig,style)
in
if dst=
nil
then {dfdop}
union msdescs
else {dst,dfdop}
union msdescs;
\
end{vdm_al}
\subsection{
Functions for the
state definition}
Each data store
in a
DFD
and each data flow
to or from an external process
is transformed
into a
state component
of the
state definition.
\begin{vdm_al}
MakeState : DFDId * DSs *
set of FlowId -> [StateDef]
MakeState(dfdid,dss,fids) ==
if dss={}
and fids={}
then nil
else let fl=MakeFieldList(dss
union fids)
in
mk_StateDef(StateIdConf(dfdid),fl);
MakeFieldList :
set of StId ->
seq of Field
MakeFieldList(ids) ==
if ids={}
then []
else let id
in set ids
in
[MakeField(id)]^MakeFieldList(ids \ {id})
measure Card;
Card:
set of StId ->
nat
Card(s) ==
card s;
MakeField : StId -> Field
MakeField(id) ==
mk_Field(StateVarConf(id),StateTypeConf(id));
\
end{vdm_al}
\subsection{
Functions for primitive MSs}
The data transformers which are
not further decomposed (they can
be considered
as being
primitive) can
be supplied
by the user
in the form
of a
mini-specification
in VDM-SL.
In the case where the user has
not supplied such a
mini-specification, a simple implicitly defined operation
is generated. Since the user has supplied only the type
information
for the data transformer (
by means
of the data flow
types) the generated definition will have the right type
with
\textbf{\ttfamily
true}
as a post-condition.
\begin{vdm_al}
MakeMSDescs : DFDSig * MSs ->
set of Definition
MakeMSDescs(dfdsig,mss) ==
if forall id
in set dom dfdsig& is_DFDId(id)
then {}
else let id
in set dom dfdsig
be st is_MSId(id)
in
let def'= if id in set dom mss
then mss(id)
else MakeOp(id,dfdsig(id))
in
{
def'} union MakeMSDescs({id} <-: dfdsig,mss);
MakeOp: MSId * (
seq of FlowId *
seq of FlowId *
State)
-> ImplOp
MakeOp(msid,mk_(din,out,dst)) ==
let partpl = MakeInpPar(din),
residtp = MakeOutPair(out),
dext = MakeExt(dst),
body = mk_ImplOpBody(
nil, mk_BoolLit(
true))
in
mk_ImplOp(OpIdConf(msid),partpl,residtp,dext,body);
MakeInpPar :
seq of FlowId ->
seq of ParType
MakeInpPar(fidl) ==
[mk_ParType(mk_PatternId(FlowIdVarConf(i)), FlowIdTypeConf(i))
| i
in seq fidl];
\
end{vdm_al}
In the function $MakeOutPair$ it should
be noticed that
if a data
transformer contains more that one data flow out
from it, it
is
necessary
to ``invent
" a new identifier to denote the result of the
data transformer ($ResultIdConf$).
\begin{vdm_al}
MakeOutPair :
seq of FlowId -> [IdType]
MakeOutPair(fidl) ==
cases len fidl:
0 ->
nil ,
1 -> mk_IdType(FlowIdVarConf(
hd fidl),
FlowIdTypeConf(
hd fidl)),
others ->
let t=mk_ProductType([FlowIdTypeConf(i) | i
in seq fidl])
in
mk_IdType(ResultIdConf(),t)
end;
MakeExt :
State ->
seq of ExtVarInf
MakeExt(dst) ==
[MakeExtVar(i)|i
in seq dst];
MakeExtVar : (StId * Mode) -> ExtVarInf
MakeExtVar(mk_(id,mode)) ==
mk_ExtVarInf(mode,VarConf(id),TypeConf(id));
\
end{vdm_al}
\subsection{
Functions for composing data transformers implicitly}
\label{depend}
An operation describing the functionality
of a DFD uses
the
operations for the lower-level DFDs.
The combination that must
be constructed depends upon the topology
of the
DFD. Whenever a data transformer receives data
from another data
transformer through a data flow (
in the same DFD) this dependency
must
be incorporated
in the combination,
by using the output value
from the first data transformer (
and possibly changed
state
component(s))
as input
for the second data transformer. However,
since a data transformer
in principle
is a loose construct (see
\cite{Wieth89}
for a thorough
treatment
of the semantics
of looseness)
it
is necessary when generating
pre and
post-conditions
to take this possible looseness into
account. This
is done
by specifying that there must exist an output
value (
and possibly one
or more changed
state values) such that the
post-condition
of the first data transformer
is fulfilled
and then
use this value (
or values)
for the data transformer which depends upon the
first one (see \cite{Plat&91a}).
By means
of three small examples we will illustrate
what has
to be taken into account
to describe the functionality
of a
DFD
as a whole.
\subsubsection*{Example 1}
Consider the \DFD\
in figure~\ref{example1}.
%\makefigure{example1}{DFD
for example 1}{example1}
It
is a simple
\DFD\ consisting
of two data transformers $P$
and $Q$,
each having one input data flow ($a$
and $b$ respectively)
and one
output data flow ($b$
and $c$ respectively).
$Q$ receives data
from $P$
and thus
$Q$ depends on $P$. When this \DFD\
is intended
to model a sequential
system it
is
obvious that $P$ must
be executed before $Q$ can
be executed. This
dependency between $P$
and $Q$ also can
be found
in the pre-
and post-condition
of the composite \DFD:
%\begin{vdm}
%\begin{op}[i]{PQ}
%\parms{a: A}[c: C]
%\begin{precond}
%\
exists{b : B}\\
% {pre-P(a) \
And\\
% post-P(a, b) \
And \\
% pre-Q(b)}
%\
end{precond}
%\begin{postcond}
%\
exists{b : B}\\
% {pre-P(a) \
And
% post-P(a, b) \
And \\
% pre-Q(b) \
And
% post-Q(b, c)}
%\
end{postcond}
%\
end{op}
%\
end{vdm}
\begin{lstlisting}
PQ(a: A) c : C
pre exists b : B & pre_P(a)
and
post_P(a,b)
and
pre_Q(b)
post exists b : B & pre_P(a)
and
post_P(a,b)
and
pre_Q(b)
and
post_Q(b,c)
\
end{lstlisting}
It
is necessary
to quote the post-condition\footnote{%
`Quoting
' pre- and post-conditions of (implicitly defined) functions and
operations is a {\small VDM} technique
to `invoke
' other
functions or operations from within a pre-
or post-condition (i.e. a
predicate): each implicitly defined function
or operation $f$ has
associated boolean {\em
functions} $pre-f$
and $post-f$ which, given the
appropriate arguments, yield $
true$
if the pre-
or post-condition respectively
of $f$ holds
for those arguments,
and $
false$ otherwise.
A quoted pre-condition
of an operation takes
the input arguments
of the operation
and the
state components
used
by the operation
as its arguments.
A quotation
of a post-condition
of an operation first takes
the input arguments
of the operation,
then some arguments
representing the
values of the
state components before the operation
is
executed, the output
result of the operation,
and finally the
new state
components (only those
to which the operation has write access).%
}
of $P$
to
produce a value that must satisfy the pre-condition
of $Q$. Since $P$
may
be loosely
specified there may
be several
values satisfying the
post-condition
of $P$ given some argument $a$. However, since only
some
of these
values might satisfy the pre-condition
of $Q$ an
existential quantification over this `internal data flow
', $b$, is
necessary.
Alternative solutions can
be envisaged, differing
in the strength
of the constraints put upon the combination.
\noindent $\Box$\\
\subsubsection*{Example 2}
Example~1
is now expanded
by introducing a data store that both
data transformer $P$
and data transformer $Q$ have write access
to.
This \DFD\
is given
in figure~\ref{example2}.
The data store $ds$
is -- as has been mentioned -- interpreted as a state
component.
%\makefigure{example2}{DFD
for example 2}{example2}
This composite \DFD\ can
be specified by the following implicit
definition:
%\begin{vdm}
%\begin{op}[i]{PQ_{DS}}
%\parms{a: A}[c: C]
%\
ext{\
Wr ds: DS\\}
%\begin{precond}
%\
exists{b : B, ds
' : DS}\\
% {pre-P(a, ds) \
And\\
% post-P(a, ds, b, ds
') \And \\
% pre-Q(b, ds
')}
%\
end{precond}
%\begin{postcond}
%\
exists{b : B, ds
' : DS}\\
% {pre-P(a, ~{ds}) \
And
% post-P(a, ~{ds}, b, ds
') \And \\
% pre-Q(b, ds
') \And
% post-Q(b, ds
', c, ds)}
%\
end{postcond}
%\
end{op}
%\
end{vdm}
\begin{lstlisting}
PQ_DS(a: A) c : C
wr ds : DS
pre exists b : B, ds
' : DS &
pre_P(a, ds)
and
post_P(a,ds,b,ds
') and
pre_Q(b,ds
')
post exists b : B, ds
' : DS &
pre_P(a,ds~)
and
post_P(a,ds~,b.ds
') and
pre_Q(b,ds
') and
post_Q(b,ds
',c,ds)
\
end{lstlisting}
It
is necessary
to introduce an intermediate
state component, $ds
'$, which holds the value of $ds$ in between execution of the different data
transformers, $P$
and $Q$. This situation occurs when several data
transformers are allowed
to modify the same data store.
In addition, this example illustrates another technicality that must
be taken into account
in the transformation
from \DFD s
to \VDM. The
value
of the
state component, $ds$, before activation
of the operation
is referred
to differently inside the pre-condition (
as $ds$)
and the
post-condition (
as $~{ds}$). When a pre-
or post-condition (using
an old
state value)
is quoted it
is necessary
to supply information
about whether it was quoted inside a pre-condition
or inside a
post-condition.
\noindent $\Box$\\
\subsubsection*{Example 3}
The \DFD\
from example~2
is now expanded
by adding an extra data
transformer, $R$, which also modifies data store $ds$, but
otherwise
is not connected
to the two other data transformers ($P$
and
$Q$). The \DFD\
is given
in figure~\ref{example3}.
%\makefigure{example3}{DFD
for example 3}{example3}
Although the \DFD\ at first sight still looks rather simple, it turns
out that the \VDM\ specification
for the \DFD\
is quite complicated. The \DFD\
is illustrative
for the situation
in which
the {\em writer}
of the \DFD\ may understand it
differently than the {\em reader}
of the \DFD. The ambiguity comes
from the fact that nothing
is said about
in which order the three data
transformers should modify the data store. Maybe it
is not important,
but maybe it
is essential that one specific execution order
is chosen
in the implementation.
The notation `$*: DS$
' (in the figure)
means that a value
of type $DS$ will
be used at this
point, but we don
't know exactly {\em which} value that will be. Consider
$P$
and $R$. One
of them uses the old value
of $ds$
in the quotation
of its post-condition, but we don
't know which one because
that depends on the execution order.
The possible execution orders are visible
in the
generated \VDM\ specification.
The following implicit definition
of the composite \DFD\ can
be generated:
%\begin{vdm}
%\begin{op}[i]{PQR_{DS}}
%\parms{a: A, d: D}[r: C \X E]
%\
ext{\
Wr ds : DS\\}
%\begin{precond}
%\
exists{b : B, c : C, e : E, ds
', ds'' : DS}\\ {%
%\lineup[c]{(}{pre-R(d, ds) \
And post-R(d, ds, e, ds
') \And \\
% pre-P(a, ds
') \And post-P(a, ds', b, ds
'') \
And pre-Q(b, ds
''))} \
Or\\
%\lineup[c]{(}{pre-P(a, ds) \
And post-P(a, ds, b, ds
') \And \\
% pre-R(d, ds
') \And post-R(d, ds', e, ds
'') \
And pre-Q(b, ds
''))} \
Or\\
%\lineup[c]{(}{pre-P(a, ds) \
And post-P(a, ds, b, ds
') \And \\
% pre-Q(b, ds
') \And post-Q(b, ds', c, ds
'') \
And pre-R(d, ds
''))}}
%\
end{precond}
%\begin{postcond}
%\
Let (c, e) = r
%\Lin\\
%\
exists{b:B, ds
', ds'' : DS}\\
%{\lineup[c]{(}{pre-R(d, ~{ds}) \
And post-R(d, ~{ds}, e, ds
') \And
% pre-P(a, ds
') \And \\ post-P(a, ds', b, ds
'') \
And
% pre-Q(b, ds
'') \
And post-Q(b, ds
'', c, ds))} \
Or\\
%\lineup[c]{(}{pre-P(a, ~{ds}) \
And post-P(a, ~{ds}, b, ds
') \And
% pre-R(d, ds
') \And \\ post-R(d, ds', e, ds
'') \
And
% pre-Q(b, ds
'') \
And post-Q(b, ds
'', c, ds))} \
Or\\
%\lineup[c]{(}{pre-P(a, ~{ds}) \
And post-P(a, ~{ds}, b, ds
') \And
% pre-Q(b, ds
') \And \\ post-Q(b, ds', c, ds
'') \
And
% pre-R(d, ds
'') \
And post-R(d, ds
'', e, ds))}}
%\
end{postcond}
%\
end{op}
%\
end{vdm}
\begin{lstlisting}
PQR_DS(a : A, d : D) r : C * E
wr ds : DS
pre exists b : B, c : C, e : E, ds
', ds'' : DS &
(pre_R(d, ds)
and post_R(d, ds, e, ds
') and
pre_P(a, ds
') and post_P(a, ds', b, ds
'')
and
pre_Q(b, ds
''))
or
(pre_P(a, ds)
and post_P(a, ds, b, ds
') and
pre_R(d, ds
') and post_R(d, ds', e, ds
'')
and
pre_Q(b, ds
''))
or
(pre_P(a, ds)
and post_P(a, ds, b, ds
') and
pre_Q(b, ds
') and post_Q(b, ds', c, ds
'')
and
pre_R(d, ds
''))
post let (c, e) = r
in
exists b:B, ds
', ds'' : DS &
(pre_R(d, ds~)
and post_R(d, ds~, e, ds
') and
pre_P(a, ds
') and post_P(a, ds', b, ds
'')
and
pre_Q(b, ds
'')
and post_Q(b, ds
'', c, ds))
or
(pre_P(a, ds~)
and post_P(a, ds~, b, ds
') and
pre_R(d, ds
') and post_R(d, ds', e, ds
'')
and
pre_Q(b, ds
'')
and post_Q(b, ds
'', c, ds))
or
(pre_P(a, ds~)
and post_P(a, ds~, b, ds
') and
pre_Q(b, ds
') and post_Q(b, ds', c, ds
'')
and
pre_R(d, ds
'')
and post_R(d, ds
'', e, ds))
\
end{lstlisting}
The post-condition shows that there are three possible
execution orders: $[P, Q, R]$, $[P, R, Q]$
and $[R, P, Q]$.
The pre-
and post-conditions defined above ensure that at least one
possible execution order can
be used.
$r$
is a
new name, introduced
to denote the output
as a whole.
\noindent $\Box$\\
Below, we present the
functions that are used
to compose
data transformers into implicit specifications. These
functions illustrate how the problematic issues
from the three
examples above are dealt
with.
\begin{vdm_al}
MakeDFDOp: DFDId * DFDTopo * DFDSig * (<EXPL>|<IMPL>) ->
OpDef
MakeDFDOp(dfdid,dfdtopo,dfdsig,style) ==
if style=<EXPL>
then MakeDFDExplOp(dfdid,dfdtopo,dfdsig)
else MakeDFDImplOp(dfdid,dfdtopo,dfdsig)
pre if style=<EXPL>
then pre_MakeDFDExplOp(dfdid,dfdtopo,dfdsig)
else pre_MakeDFDImplOp(dfdid,dfdtopo,dfdsig);
MakeDFDImplOp : DFDId * DFDTopo * DFDSig -> ImplOp
MakeDFDImplOp(dfdid,dfdtopo,dfdsig) ==
let mk_(din,out,dst)=dfdsig(dfdid)
in
let partpl = MakeInpPar(din),
residtp = MakeOutPair(out),
dext = MakeExt(dst),
body = MakeImplOpBody(dfdid,dfdtopo,dfdsig)
in
mk_ImplOp(OpIdConf(dfdid),partpl,residtp,dext,body)
pre dfdid
in set dom dfdsig
and
pre_MakeImplOpBody(dfdid,dfdtopo,dfdsig);
\
end{vdm_al}
The function $MakeImplOpBody$
is used
to generate both the pre-condition
and the post-condition
of an implicit operation definition.
In order
to take intermediate data store
values into account,
$MakeImplOpBody$
and its auxiliary
functions will use a
map from state
components
to the current number
of intermediate
values ($intm$).
The
map is initialized
by mapping
all state components
to zero
(indicating that no intermediate
state values have been introduced
yet)%
\footnote{The configuration function $StateVarIntConf$
inserts a number
of quotes corresponding
to the number
of the
intermediate value,
as it was done
in the examples.}.
In addition, a
map $maxm$
with the same domain
of
state components
is used
to ensure that a
post-condition uses the
state after an operation
as the last
of a
series
of intermediate
state components. Each
state
component
in $maxm$
is mapped
to the number
of data transformers
having write access (
and thus potentially introduce an
intermediate
state value)
to that
state component.
\begin{vdm_al}
MakeImplOpBody : DFDId * DFDTopo * DFDSig -> ImplOpBody
MakeImplOpBody(dfdid,dfdtopo,dfdsig) ==
let intm = {stid |-> 0|mk_(stid,-)
in set
CollectStIds(
rng dfdsig)},
maxm = {stid |-> Reduce(NoOfWr(
rng dfdsig,stid))
| mk_(stid, -)
in set
CollectStIds(
rng dfdsig)},
dpre = MakePreExpr(dfdid,dfdtopo,dfdsig,intm,maxm),
dpost = MakePostExpr(dfdid,dfdtopo,dfdsig,intm,maxm)
in
mk_ImplOpBody(dpre,dpost)
pre let intm = {stid |-> 0|mk_(stid,-)
in set
CollectStIds(
rng dfdsig)},
maxm = {stid |-> Reduce(NoOfWr(
rng dfdsig,stid))
| mk_(stid,-)
in set
CollectStIds(
rng dfdsig)}
in
pre_MakePreExpr(dfdid,dfdtopo,dfdsig,intm,maxm)
and
pre_MakePostExpr(dfdid,dfdtopo,dfdsig,intm,maxm)
\
end{vdm_al}
The $IntM$ domain
is an auxiliary domain which
is used
in the formal
transformation
from SA
to VDM. It
is used
to provide information
about intermediate
state values.
\begin{vdm_al}
types
IntM =
map StId
to nat
\
end{vdm_al}
The function $MakePreExpr$
is used
to generate the pre-condition
of an
implicit operation body. The function will first determine whether an
existential quantified expressions
is needed
%(which
is the case
if there are independent
%partitions consisiting
of more than one data transformer each)
by calling $QuantNec$,
and depending on that, create either a existential
quantified expression,
or just the predicate part
of such an expression.
\begin{vdm_al}
functions
MakePreExpr: DFDId * DFDTopo * DFDSig * IntM * IntM ->
Expr
MakePreExpr(dfdid,dfdtopo,dfdsig,intm,maxm) ==
let mk_(-,out,dst)=dfdsig(dfdid)
in
let fids = NeedsQuant(dfdtopo,dfdsig,{},{}),
pred = MakePrePred(dfdtopo,dfdsig,intm,maxm)
in
if QuantNec(out,dst,fids,intm,maxm)
then let bind = MakeExistsBind(fids,dst,intm,
maxm,<
PRE>)
in
mk_ExistsExpr(bind,pred)
else pred
pre dfdid
in set dom dfdsig;
\
end{vdm_al}
The function $MakePrePred$
is used
to create the `body
' of the pre-condition
of an implicit operation. First,
all possible orders
of execution are
determined.
Then,
for each data transformer it
is ensured that its pre-condition
can
be satisfied
by generating a predicate
in which the pre-condition
of that
data transformer
is quoted
in a context
in which
all its predecessors
in a possible executation order have
been executed.
Finally,
all such predicates
or combined
in a disjunction.
\begin{vdm_al}
MakePrePred : DFDTopo * DFDSig * IntM * IntM -> Expr
MakePrePred(dfdtopo,dfdsig,intm,maxm) ==
let eos=ExecutionOrders(dfdtopo)
in
DBinOp(<
OR>,{MakePreForEO(piseq,dfdsig,intm,maxm)
|piseq
in set eos});
\
end{vdm_al}
The function $MakePreForEO$ generates a pre-expression
for a specific
execution order $piseq$. An application
of both the
quoted
pre and the quoted post-condition
of the first data transformer
in the execution order
is generated (
by $MakeQuotedApply$)
and then $MakePreForEO$
is called
recursively
with the remainder
of the data transformers
in $piseq$.
A collection
of intermediate
state values $intm
'$ is constructed in each
recursion step
in order
to use the correct intermediate
state values
in the construction
of a quotation
for an operation.
All quotations are combined
in a conjunction.
\begin{vdm_al}
MakePreForEO:
seq1 of ProcId * DFDSig * IntM * IntM ->
Expr
MakePreForEO(piseq,dfdsig,intm,maxm) ==
let nid=
hd piseq
in
let intm
'={stid |-> if mk_(stid, ) in set
CollectStIds({dfdsig(nid)})
then intm(stid) + 1
else intm(stid)
| stid
in set dom intm}
in
let dpre = MakeQuotedApply(nid,dfdsig(nid),intm
',maxm,
<
PRE>,<
PRE>),
dpost = MakeQuotedApply(nid,dfdsig(nid),intm
',maxm,
<
PRE>,<
POST>)
in
if len piseq=1
then dpre
else let pred=mk_BinaryExpr(dpre,<
AND>,dpost)
in
mk_BinaryExpr(pred,<
AND>,
MakePreForEO(
tl piseq,dfdsig,
intm
',maxm));
\
end{vdm_al}
$MakePostExpr$
is used
to generate the post-condition
of an implicit operation.
When a DFD has more than one output, these outputs are combined into
a tuple expression. A
new name
for this tuple expression
is created
by
generating a let-expression. $MakePostExpr$ first determines
whether such a let-expression should
be generated.
Then, the body
of the post-expression
is generated
by calling $MakeInExpr$.
\begin{vdm_al}
MakePostExpr: DFDId * DFDTopo * DFDSig * IntM * IntM ->
Expr
MakePostExpr(dfdid,dfdtopo,dfdsig,intm,maxm) ==
let mk_(-,out,dst)=dfdsig(dfdid),
fids = NeedsQuant(dfdtopo,dfdsig,
elems out,{}),
body = MakeInExpr(out,dst,fids,dfdtopo,dfdsig,
intm,maxm)
in
if len out<= 1
then body
else mk_LetExpr(MakePattern(out),ResultIdConf(),body)
pre let mk_(-,out,dst)=dfdsig(dfdid),
fids = NeedsQuant(dfdtopo,dfdsig,
elems out,{})
in
pre_MakeInExpr(out,dst,fids,dfdtopo,dfdsig,
intm,maxm);
\
end{vdm_al}
The function $MakeInExpr$ operates
in much the same way
as $MakePreExpr$ does
for the generation
of pre-conditions. The function examines whether an
existential quantification
is needed,
and if this
is the case such a
quantified expression
is generated. The remainder
of the post-condition
is
generated
by calling $MakePostPred$.
\begin{vdm_al}
MakeInExpr:
seq of FlowId *
State *
set of FlowId *
DFDTopo * DFDSig * IntM * IntM -> Expr
MakeInExpr(out,dst,fids,dfdtopo,dfdsig,intm,maxm) ==
let pred=MakePostPred(dfdtopo,dfdsig,intm,maxm)
in
if QuantNec(out,dst,fids,intm,maxm)
then let bind = MakeExistsBind(fids,dst,intm,maxm,
<
POST>)
in
mk_ExistsExpr(bind,pred)
else pred
pre pre_MakeExistsBind(fids,dst,intm,maxm,<
POST>);
\
end{vdm_al}
The function $MakePostPred$
is used
to create the `body
' of the post-condition
of an implicit operation. First,
all possible orders
of execution are
determined,
and for each execution order a conjunction
of quoted function
applications are generated using the intermediate
state values (this
is done
in $MakePostForEO$).
The separate conjunctions are
then combined
in one large disjunction,
in this way specifying that the implementor can choose either one
of the
execution orders
to implement the DFD.
\begin{vdm_al}
MakePostPred : DFDTopo * DFDSig * IntM * IntM -> Expr
MakePostPred(dfdtopo,dfdsig,intm,maxm) ==
let eos=ExecutionOrders(dfdtopo)
in
DBinOp(<
OR>,{MakePostForEO(piseq,dfdsig,intm,maxm)
|piseq
in set eos});
\
end{vdm_al}
The function $MakePostForEO$ generates a post-expression
for a specific
execution order $piseq$. An application
of both the
quoted
pre and the quoted post-condition
of the first data transformer
in the execution order
is generated (
by $MakeQuotedApply$)
and then $MakePostForEO$
is called
recursively
with the remainder
of the data transformers
in $piseq$.
A collection
of intermediate
state values $intm
'$ is constructed in each
recursion step
in order
to use the correct intermediate
state values
in the construction
of a quotation
for an operation.
All quotations are combined
in a conjunction.
\begin{vdm_al}
MakePostForEO:
seq1 of ProcId * DFDSig * IntM * IntM ->
Expr
MakePostForEO(piseq,dfdsig,intm,maxm) ==
let nid=
hd piseq
in
let intm
'={stid |-> if mk_(stid, ) in set
CollectStIds({dfdsig(nid)})
then intm(stid) + 1
else intm(stid)
| stid
in set dom intm}
in
let dpre = MakeQuotedApply(nid,dfdsig(nid),intm
',maxm,
<
POST>, <
PRE>),
dpost = MakeQuotedApply(nid,dfdsig(nid),intm
',maxm,
<
POST>,<
POST>)
in
if len piseq=1
then mk_BinaryExpr(dpre,<
AND>,dpost)
else let pred=mk_BinaryExpr(dpre,<
AND>,dpost)
in
mk_BinaryExpr(pred,<
AND>,MakePostForEO(
tl piseq,dfdsig,
intm
',maxm))
pre let nid=
hd piseq
in
nid
in set dom dfdsig
and
pre_MakeQuotedApply(nid,dfdsig(nid),intm,maxm,
<
POST>,<
PRE>)
and
pre_MakeQuotedApply(nid,dfdsig(nid),intm,maxm,
<
POST>,<
POST>);
\
end{vdm_al}
The function $MakeExistsBind$
is used
by both $MakePreExpr$
and
$MakeInExpr$
for the construction
of a multiple type binding (
to be used
in an
existential quantification),
and a correspondingly updated collection
of intermediate
state values.
%The intermediate
state
%
values are first updated ($intm$)
by increasing each
state component
in $
st$
%(which has write access)
by one,
if it
is not equivalent
to the last
%one.
Two lists ($outl$
and $stl$)
of pairs (the variable name
and
its type) are created
in which the intermediate
state values
(collected
in $intm$) are taken into account.
Then a multiple type binding
with these two lists
is returned.
\begin{vdm_al}
MakeExistsBind:
set of FlowId *
State * IntM * IntM *
(<
PRE>|<
POST>) -> MultTypeBind
MakeExistsBind(fs,dst,intm,maxm,c) ==
let outl = MakeTypeBindList(fs),
stl = [
let mk_(s,-)=i,
p = MakePatternIds(s,intm(s)+1,maxm(s),c)
in
mk_TypeBind(p,StateTypeConf(s))
|i
in seq dst
&
let mk_(-,m)=i
in m=<READWRITE>]
in
mk_MultTypeBind(outl^stl)
pre forall mk_(s,<READWRITE>)
in seq dst&
s
in set dom intm
and s
in set dom maxm;
\
end{vdm_al}
The function $ExecutionOrders$ generates a
set of `possible
execution orders
'. An
execution order
is a sequence
of $ProcId$s. The order
of $ProcId$s
in such
an execution order
is a valid order
in which the data transformers
in a
DFD
with topology $dfdtopo$ can
be executed.
\begin{vdm_al}
ExecutionOrders: DFDTopo ->
set of seq1 of ProcId
ExecutionOrders(dfdtopo) ==
let top={mk_(fid,tid)
|mk_(fid,tid)
in set rng dfdtopo &
(is_DFDId(fid)
or is_MSId(fid)
or (fid =
nil))
and
(is_DFDId(tid)
or is_MSId(tid)
or (tid =
nil))},
top2={mk_(fid,tid)|mk_(fid,tid)
in set rng dfdtopo &
(is_DFDId(fid)
or is_MSId(fid))
and
(is_DFDId(tid)
or is_MSId(tid))}
in
let piset=
dunion {{pi_1,pi_2}
|mk_(pi_1,pi_2)
in set top}\{
nil}
in
{piseq | piseq
in set PossibleSeqs(piset) &
forall i,j
in set inds piseq &
j<i => (piseq(j)
not in set
TransClosure(piseq(i),top2,{}))};
\
end{vdm_al}
$MakeQuotedApply$ generates the application
of the quotation
of
a
pre or a post-condition
of an operation. Note that the configuration
function $StateVarIntConf$
is given information about where it
is
quoted
from. The necessity
for this was shown
in example~2.
\begin{vdm_al}
MakeQuotedApply: (DFDId|MSId) * Signature * IntM * IntM *
(<
PRE>|<
POST>) * (<
PRE>|<
POST>) -> Apply
MakeQuotedApply(id,mk_(din,out,dst),intm,maxm,c,c2) ==
let inarg = [FlowIdVarConf(i)|i
in seq din],
oldstarg = [
let mk_(s,m)=i
in
if m=<READ>
then StateVarIntConf(s,intm(s),
maxm(s),c)
else StateVarIntConf(s,intm(s) - 1,
maxm(s),c)
|i
in seq dst],
outarg = [FlowIdVarConf(i)|i
in seq out],
starg = [
let mk_(s,-)=i
in
StateVarIntConf(s,intm(s),maxm(s),c)
|i
in seq dst &
let mk_(-,m)=i
in m=<READWRITE>]
in
if c2=<
PRE>
then mk_Apply(
"pre_"^OpIdConf(id),inarg^oldstarg)
else mk_Apply(
"post_"^OpIdConf(id),inarg^oldstarg^
outarg^starg)
pre forall mk_(s,m)
in seq dst&
s
in set dom intm
and
s
in set dom maxm
and
m=<READWRITE> => intm(s)>0;
\
end{vdm_al}
\subsection{
Functions for composing data transformers explicitly}
The explicit
definitions of
operations for composing data transformers
in a DFD are generated
following the same dependency strategy which
is used
for
generating the implicit
definitions. The principle
for combining the
data transformers uses the same dependency information
from the
DFD. However, since the
state of the DFD
is not explicitly mentioned
in the call
of an operation, there
is no problem
with intermediate
state values for the explicit
definitions. Thus, the explicit
definitions will
in general
be shorter
and easier
to read than the
implicit ones. The different execution orders are dealt
with by using the
non-deterministic statement\footnote{VDM-SL has a non-deterministic statement which
takes a
set of statements
and executes each
of them them
in a
non-deterministic order.}.
In this way the choice
of execution order
is left open.
\subsubsection*{Example 4}
Before presenting the formal description
of how \DFD s
as a whole can
be
transformed into explicit operation
definitions, we show how
the \DFDs\
from the first three examples can
be described explicitly.
The first \DFD\
from figure~\ref{example1} can
be specified by the following explicit
operation definition:
%\begin{vdm}
%\begin{op}[e]{PQ}
%\signature{A \Oto C}
%\parms{a}
%\
Def b = P(a)
%\Din
%\
Def c = Q(b)
%\Din
%\
return{c}
%\
end{op}
%\
end{vdm}
\begin{lstlisting}
PQ: A ==> C
PQ(a) ==
def b = P(a)
in
def c = Q(b)
in
return c
\
end{lstlisting}
\noindent
Def-statements\footnote{A def-statement corresponds
to a let-statement
(
or let-expression) except that it
is legal at the right-hand-side
of
the equal sign
to use an operation call that may modify the
state.}
are used
to introduce the (intermediate) data flows.
For the \DFD\
in figure~\ref{example2} the following explicit operation can
be
generated:
%\begin{vdm}
%\begin{op}[e]{PQ_{DS}}
%\signature{A \Oto C}
%\parms{a}
%\
Def b = P(a)
%\Din
%\
Def c = Q(b)
%\Din
%\
return{c}
%\
end{op}
%\
end{vdm}
\begin{lstlisting}
PQ_DS: A ==> C
PQ_DS(a) ==
def b = P(a)
in
def c = Q(b)
in
return c
\
end{lstlisting}
\noindent
This operation
is equivalent
to the one generated
for the \DFD\
in example~\ref{example1}, because
the
state components that are modified
by the different
operation need
not be explicitly mentioned
in the call
of these
operations.
In this respect, explicit
operations in \VDMSL\ are very much similar
to procedures
in imperative programming languages accessing global
variables.
The following explicit operation can
be generated
for the \DFD\
in figure~\ref{example3}:
\begin{lstlisting}
PQR_DS: A * D ==> C * E
PQR_DS(a,d) ==
||
((
def b = P(a)
in
def c = Q(b)
in
def e = R(d)
in
return mk_(c,e)),
(
def e = R(d)
in
def b = P(a)
in
def c = Q(b)
in
return mk_(c,e)),
(
def b = P(a)
in
def e = R(d)
in
def c = Q(b)
in
return mk_(c,e))
)
\
end{lstlisting}
%\begin{vdm}
%\begin{op}[e]{PQR_{DS}}
%\signature{A \X D \Oto C \X E}
%\parms{a, d}
%\begin{nondetstmt}
%\lineup[c]{(}
%{\
Def b = P(a)
%\Din
%\
Def c = Q(b)
%\Din
%\
Def e = R(d)
%\Din
%\
return{mk-(c, e)}),}\\
%\lineup[c]{(}
%{\
Def e = R(d)
%\Din
%\
Def b = P(a)
%\Din
%\
Def c = Q(b)
%\Din
%\
return{mk-(c, e)}),}\\
%\lineup[c]{(}
%{\
Def b = P(a)
%\Din
%\
Def e = R(d)
%\Din
%\
Def c = Q(b)
%\Din
%\
return{mk-(c, e)})}
%\
end{nondetstmt}
%\
end{op}
%\
end{vdm}
\noindent
The three different execution orders
are incorporated
in a
non-deterministic statement. It
is necessary
to use a
return
statement at the
end of each sequence statement
in the
nondeterministic statement (each represents a possible execution order)
to ensure that a correct
return value
is created.
\noindent $\Box$\\
The function used
to create
operations for \DFD s
in
the explicit style
is called $MakeDFDExplOp$.
The strategy
is somewhat similar
to the one that
has been used
for the implicit style. Here we also have a number
of
possible execution orders that must
be taken into account.
\begin{vdm_al}
MakeDFDExplOp : DFDId * DFDTopo * DFDSig -> ExplOp
MakeDFDExplOp(dfdid,dfdtopo,dfdsig) ==
let mk_(din,-,-) = dfdsig(dfdid),
eos = ExecutionOrders(dfdtopo),
intm = {stid |-> 0
| mk_(stid,-)
in set
CollectStIds(
rng dfdsig)},
maxm = {stid |-> Reduce(NoOfWr(
rng dfdsig,stid))
|mk_(stid,-)
in set CollectStIds(
rng dfdsig)}
in
let optype = MakeOpType(dfdsig(dfdid)),
parms = [mk_PatternId(FlowIdVarConf(i))
|i
in seq din],
bodys = {MakeStmtForEO(piseq,dfdid,dfdsig)
|piseq
in set eos},
dpre = MakePreExpr(dfdid,dfdtopo,dfdsig,intm,maxm)
in
let body = MakeNonDetStmt(bodys)
in
mk_ExplOp(OpIdConf(dfdid),optype,parms,body,dpre)
pre dfdid
in set dom dfdsig
and
let intm = {stid |-> 0
|mk_(stid,-)
in set CollectStIds(
rng dfdsig)},
maxm = {stid |-> Reduce(NoOfWr(
rng dfdsig,stid))
|mk_(stid,-)
in set CollectStIds(
rng dfdsig)}
in
pre_MakePreExpr(dfdid,dfdtopo,dfdsig,intm,maxm)
and
forall piseq
in set ExecutionOrders(dfdtopo)&
pre_MakeStmtForEO(piseq,dfdid,dfdsig);
\
end{vdm_al}
The function $MakeExplOpBody$
is defined recursively.
In each
recursion step one
data transformer
is processed until
all data transformers
(collected
in $pids$)
in the given partition $p$ have been
incorporated. The strategy
is the same
as for $MakePreExpr$
and
$MakePostExpr$ where a
new (independent) data transformer ($nid$)
is
chosen. The function $MakeCallAndPat$ creates
a call
of the operation
for the given
data transformer
and the corresponding pattern which the call must
be matched against.
If the operation returns a value, the call
is used
in a define statement. Otherwise it
is a call statement
which must
be included
as a part
of a sequence
of statements.
\begin{vdm_al}
MakeStmtForEO:
seq1 of ProcId * DFDId * DFDSig -> Stmt
MakeStmtForEO(piseq,dfdid,dfdsig) ==
let nid=
hd piseq
in
let mk_(call,pat) = MakeCallAndPat(nid,dfdsig(nid)),
kind = FindKind(dfdsig(nid))
in
if len piseq=1
then let mk_(-,out,-)=dfdsig(dfdid)
in
let ret=mk_Return(MakeResult(out))
in
if kind=<OPRES>
then mk_DefStmt(pat,call,ret)
else mk_Sequence([call,ret])
else let rest=MakeStmtForEO(
tl piseq,dfdid,dfdsig)
in
if kind=<OPRES>
then mk_DefStmt(pat,call,rest)
else if is_Sequence(rest)
then let mk_Sequence(sl)=rest
in
mk_Sequence([call]^sl)
else mk_Sequence([call,rest])
pre hd piseq
in set dom dfdsig;
MakeCallAndPat : (DFDId|MSId) * Signature -> Call * [Pattern]
MakeCallAndPat(id,mk_(din,out,-)) ==
let inarg = [FlowIdVarConf(i)|i
in seq din],
outarg = [FlowIdVarConf(i)|i
in seq out]
in
mk_(mk_Call(OpIdConf(id),inarg),MakePattern(outarg));
FindKind : Signature -> <OPRES>|<OPCALL>
FindKind(sig) ==
cases sig:
mk_(-,[],-) -> <OPCALL>,
others -> <OPRES>
end;
MakePattern :
seq of Id -> [Pattern]
MakePattern(idl) ==
cases len idl:
0 ->
nil ,
1 -> mk_PatternId(
hd idl),
others -> mk_TuplePattern([mk_PatternId(i) | i
in seq idl])
end;
MakeResult :
seq1 of Id -> Expr
MakeResult(idl) ==
if len idl=1
then FlowIdVarConf(
hd idl)
else mk_TupleConstructor([FlowIdVarConf(i) | i
in seq idl]);
\
end{vdm_al}
\subsection{General Auxiliary
Functions}
The function $DBinOp$ generates an expression
by distributing a binary operator
over a
set of expressions.
\begin{vdm_al}
DBinOp : BinaryOp * set1
of Expr -> Expr
DBinOp(op,es) ==
let e
in set es
in
if card es=1
then e
else mk_BinaryExpr(e,op,DBinOp(op, es \ {e}));
\
end{vdm_al}
The function $CollectExtDFs$
is intended
to collect the external data
flow identifiers
from the topology
of a DFD.
\begin{vdm_al}
CollectExtDFs : DFDTopo ->
set of FlowId
CollectExtDFs(dfdtopo) ==
{fid|fid
in set dom dfdtopo
&
let mk_(pid_1,pid_2)=dfdtopo(fid)
in
is_EPId(pid_1)
or is_EPId(pid_2)};
NeedsQuant: DFDTopo * DFDSig *
set of FlowId *
set of ProcId ->
set of FlowId
NeedsQuant(dfdtopo,dfdsig,notneeded,pids) ==
let top={mk_(fid,tid)|mk_(fid,tid)
in set rng dfdtopo &
(is_DFDId(fid)
or is_MSId(fid))
and
(is_DFDId(tid)
or is_MSId(tid))}
in
if dom dfdsig=pids
then {}
else let pid
in set dom dfdsig \ pids
in
if TransClosure(pid,top,{})={}
and
EquivClass(top,{pid})=
dom dfdsig
then NeedsQuant(dfdtopo,dfdsig,notneeded,
pids
union {pid})
else let mk_(-,out,-)=dfdsig(pid)
in
NeedsQuant(dfdtopo,dfdsig,notneeded,
pids
union {pid})
union
elems out \ notneeded;
\
end{vdm_al}
The function $QuantNec$
is responsible
for determining whether it
is
necessary
to use an existential quantification at a given place
in a
post-condition.
\begin{vdm_al}
QuantNec:
seq of FlowId *
State *
set of FlowId *
IntM * IntM ->
bool
QuantNec(out,dst,fids,intm,maxm) ==
fids <> {}
or
-- (exists id in seq out& id in set fids) or
(
exists mk_(s,m)
in seq dst&
m=<READWRITE>
and intm(s)<maxm(s))
pre forall mk_(s,-)
in seq dst&
s
in set dom intm
and s
in set dom maxm;
MakeTypeBindList :
set of FlowId ->
seq of TypeBind
MakeTypeBindList(fids) ==
if fids={}
then []
else let fid
in set fids
in
let pat = [mk_PatternId(FlowIdVarConf(fid))],
first=mk_TypeBind(pat,FlowIdTypeConf(fid))
in
[first]^MakeTypeBindList(fids \ {fid})
measure CardFId;
CardFId:
set of FlowId ->
nat
CardFId(s) ==
card s;
MakePatternIds: (Id | DSId) *
nat *
nat *
(<
PRE>|<
POST>) ->
seq of PatternId
MakePatternIds(id, n, max, c) ==
if (n = max)
and (c = <
POST>)
then [mk_PatternId(StateVarConf(id))]
else cases n:
0 ->
if c = <
PRE>
then [mk_PatternId(StateVarConf(id))]
else [mk_PatternId(StateOldVarConf(id))],
others -> MakePatternSeq(StateVarConf(id), n, max)
end;
MakePatternSeq: Id *
nat *
nat ->
seq of PatternId
MakePatternSeq(id, n, max) ==
if n = max
then [mk_PatternId(id ^
"'")]
else [mk_PatternId(id ^
"'")] ^
MakePatternSeq(id ^
"'", n+1, max)
pre n <= max
measure TowardsMax;
TowardsMax: Id *
nat *
nat ->
nat
TowardsMax(-,n,max) ==
max - n;
\
end{vdm_al}
The function $EquivClass$ collects
all data transformers
from a
topology which are connected
in an equivalence
class.
\begin{vdm_al}
EquivClass:
set of (ProcId * ProcId) *
set of (MSId|DFDId) ->
set of (MSId|DFDId)
EquivClass(top,ids) ==
if exists mk_(fid,tid)
in set top&
(fid
in set ids
and tid
not in set ids)
or
(tid
in set ids
and fid
not in set ids)
then let mk_(fid,tid)
in set top
be st
(fid
in set ids
and tid
not in set ids)
or
(tid
in set ids
and fid
not in set ids)
in
EquivClass(top,ids
union {fid,tid})
else ids;
\
end{vdm_al}
$MakeNonDetStmt$ takes a
set of statements,
and
generate a non-deterministic statement
from them
if there
is more than
one partition.
\begin{vdm_al}
MakeNonDetStmt :
set of Stmt -> Stmt
MakeNonDetStmt(stmts) ==
cases card stmts:
1 ->
let {s}=stmts
in s,
others -> mk_NonDetStmt(stmts)
end
pre card stmts<>0;
\
end{vdm_al}
The function $CollectStIds$ collects
all state
component identifiers
from a DFD.
\begin{vdm_al}
CollectStIds:
set of Signature ->
set of (StId * Mode)
CollectStIds(sigs) ==
dunion {
elems dst|mk_(-,-,dst)
in set sigs};
\
end{vdm_al}
The purpose
of $NoOfWr$
is to determine how many data transformers there
are
in a given partition that have write access
to a given
state component.
This information
is used
to deal
with the intermediate
state values.
\begin{vdm_al}
NoOfWr:
set of Signature * StId ->
nat
NoOfWr(sigs,stid) ==
if sigs={}
then 0
else let sig
in set sigs
in
let mk_(-,-,dst)=sig
in
if mk_(stid,<READWRITE>)
in set elems dst
then 1+NoOfWr(sigs \ {sig},stid)
else NoOfWr(sigs \ {sig},stid);
Reduce:
nat ->
nat
Reduce(n) ==
if (n = 0)
or (n = 1)
then n
else n - 1;
\
end{vdm_al}
\subsection{Configuration
functions}
\begin{vdm_al}
ModIdConf : DFDId -> Id
ModIdConf(mk_DFDId(id)) ==
id^
"Module";
StateIdConf : DFDId -> Id
StateIdConf(mk_DFDId(id)) ==
id^
"State";
DSIdConf : DSId -> Id
DSIdConf(mk_DSId(id)) ==
id;
OpIdConf : MSId | DFDId | Id -> Id
OpIdConf(id) ==
cases id:
mk_MSId(id
'),
mk_DFDId(id
') -> id',
others -> id
end;
\
end{vdm_al}
The $StateVarIntConf$ function needs
to know whether a
state component
is being referred
to in a pre-condition
or in a
post-condition
of an operation. This
is caused
by the fact that the
state before the call
of the operation
is denoted differently
in a
pre-condition than
in a post-condition (
in a pre-condition $v$ means
the
state before calling the operation,
while that
is denoted
by $~v$
in a post-condition).
\begin{vdm_al}
StateVarIntConf: (Id | DSId) *
nat *
nat * (<
PRE>|<
POST>)
-> Id
StateVarIntConf(id,n,max,c) ==
if (max=n)
and (c=<
POST>)
then StateVarConf(id)
else cases n:
0 ->
if c=<
PRE>
then StateVarConf(id)
else StateOldVarConf(id),
1 -> StateVarConf(id)^
"'",
others -> StateVarIntConf(id,n - 1,max,c)^
"'"
end;
VarConf : StId -> Id
VarConf(id) ==
if is_DSId(id)
then StateVarConf(id)
else FlowIdVarConf(id);
TypeConf : DSId|FlowId -> Id
TypeConf(id) ==
if is_DSId(id)
then StateTypeConf(id)
else FlowIdTypeConf(id);
FlowIdVarConf : Id -> Id
FlowIdVarConf(id) ==
ToLower(id);
FlowIdTypeConf : Id -> Id
FlowIdTypeConf(id) ==
ToUpper(id);
StateTypeConf : Id | DSId -> Id
StateTypeConf(id) ==
ToUpper(id);
StateVarConf : Id | DSId -> Id
StateVarConf(id) ==
ToLower(id);
StateOldVarConf : Id | DSId -> Id
StateOldVarConf(id) ==
ToLower(id)^
"old";
TypeModConf : () -> Id
TypeModConf() ==
"TypeModule";
ResultIdConf : () -> Id
ResultIdConf() ==
"r";
PossibleSeqs:
set of ProcId ->
set of seq of ProcId
PossibleSeqs(pids) ==
if pids = {}
then {}
else if card pids = 1
then {[pid]| pid
in set pids}
else let pid
in set pids
in
let rest = PossibleSeqs(pids \ {pid})
in
dunion {InsertPId(pid,
seq')
|
seq' in set rest}
measure CardPSet;
CardPSet:
set of ProcId ->
nat
CardPSet(s) ==
card s;
InsertPId: ProcId *
seq of ProcId ->
set of seq of ProcId
InsertPId(pid,
seq') ==
{
seq'(1,...,i) ^ [pid] ^ seq'(i+1,...,
len(
seq'))
| i
in set {0,...,
len(
seq')}};
ToLower: Id | DSId | DFDId | EPId | MSId -> Id
ToLower(id) ==
let realid =
cases id:
mk_DSId(id
'),
mk_DFDId(id
'),
mk_EPId(id
'),
mk_MSId(id
') -> id',
others -> id
end
in
[LowerChar(i) | i
in seq realid];
\
end{vdm_al}
The auxiliary
functions ($ToLower$
and $ToUpper$) are
to change
all letters
to lower-case
and upper-case letters respectively.
\begin{vdm_al}
LowerChar:
char ->
char
LowerChar(c) ==
cases c:
'A' ->
'a',
'B' ->
'b',
'C' ->
'c',
'D' ->
'd',
'E' ->
'e',
'F' ->
'f',
'G' ->
'g',
'H' ->
'h',
'I' ->
'i',
'J' ->
'j',
'K' ->
'k',
'L' ->
'l',
'M' ->
'm',
'N' ->
'n',
'O' ->
'o',
'P' ->
'p',
'Q' ->
'q',
'R' ->
'r',
'S' ->
's',
'T' ->
't',
'U' ->
'u',
'V' ->
'v',
'W' ->
'w',
'X' ->
'x',
'Y' ->
'y',
'Z' ->
'z',
others -> c
end;
ToUpper: Id | DSId | DFDId | EPId | MSId -> Id
ToUpper(id) ==
let realid =
cases id:
mk_DSId(id
'),
mk_DFDId(id
'),
mk_EPId(id
'),
mk_MSId(id
') -> id',
others -> id
end
in
[UpperChar(i) | i
in seq realid];
UpperChar:
char ->
char
UpperChar(c) ==
cases c:
'a' ->
'A',
'b' ->
'B',
'c' ->
'C',
'd' ->
'D',
'e' ->
'E',
'f' ->
'F',
'g' ->
'G',
'h' ->
'H',
'i' ->
'I',
'j' ->
'J',
'k' ->
'K',
'l' ->
'L',
'm' ->
'M',
'n' ->
'N',
'o' ->
'O',
'p' ->
'P',
'q' ->
'Q',
'r' ->
'R',
's' ->
'S',
't' ->
'T',
'u' ->
'U',
'v' ->
'V',
'w' ->
'W',
'x' ->
'X',
'y' ->
'Y',
'z' ->
'Z',
others -> c
end
\
end{vdm_al}
\section{Conclusions}
\label{sec:conclusions}
In this paper we have defined a semantics
for \DFDs\
by formally
specifying a transformation
from \DFDs\
to \VDM\ specifications.
In this
section we give a brief overview
of related work
in the area
of
defining semantics
for \DFDs,
and we conclude
with some
observations on our work
and some ideas
for further research.
\subsection{Related work}
When \DFDs\ were originally introduced, they were presented
as a
graphical notation. The intended semantics
of this notation
was defined verbally, but the need
for a formal base
is now more
commonly recognized, see e.g.~\cite{Hofstede&92}.
Work has been done on formalizing \DFDs,
with the intention
of either disambiguating their meaning,
or of using
the formal semantics
as a base
for a combined formal/structured method.
In \cite{Randell90} a translation back
and forth between \DFDs\
and Z specifications
is descr
ibed.
\cite{Alabiso88} contains an explanation of how \DFDs\ can manually
be transformed into an object-oriented design. The paper touches
upon some problematic issues arising in a transformation from \DFDs.
In \cite{Semmens&91c} a small example of how a \DFD\ can be transformed
in Z is presented. However, no formal semantics of the \DFDs\ is
presented and it is not clear to what extent the transformation can
be automated.
In \cite{Bruza&89} some guidelines for how semantics can be attached
to \DFDs\ are given. It is sketched how \DFDs\ can be transformed into a
Petri net variant combined with path expressions.
In \cite{Elmstrom&93} a complete semantics is provided for the Ward
and Mellor version of SA/RT by means of high-level timed Petri nets.
Here an executable subset of VDM-SL is also used to describe the
mini-specifications of an SA/RT model.
In \cite{Adler88} a semantic base for guiding the decomposition
process in the construction of a hierarchy of \DFDs\ is presented. This
work is based on graph theory in an algebraic setting.
Kevin Jones uses \VDM\ to provide a denotational style semantics of a
non-conventional machine architecture (The Manchester DataFlow Machine)
based on data flow graphs \cite{Jones87e}.
In \cite{Fraser&91} a rule-based approach for transforming \SA\ products
into \VDM\ specifications is presented. Their \VDM\ specifications are
very explicit and hard to read, mainly because of the way
decision tables have been taken into account.
Polack concentrate on the methodological aspects of combining
\SA\ notations and {\small Z}\ specifications \cite{Polack92}, the resulting
combination is known as {\small SAZ}.
Tse and Pong use extended Petri nets for formalizing \DFDs\ \cite{Tse&89}.
France discusses an algebraic approach to modeling control-extended
DFDs in~\cite{France92}.
In~\cite{Semmens&92a} an overview of several approaches to combining \SA\
techniques and notations with formal methods (including our approach) is
given.
The main result of the work presented in this paper with respect to
other work in this area is that we have been able to capture the semantics of
a \DFD\ as a whole in a compositional way at a high level of
abstraction, taking into account the whole hierarchy of \DFDs\ that is
created during an \SA\ development, which to our knowledge
has not been done before.
\subsection{Status and Perspectives}
With respect to the semantics of \DFDs\ in terms of a formal
transformation to \VDM\ specifications the following observations can be made:
\begin{itemize}
\item
An unambiguous interpretation of \DFDs\ is available, which
-- due to the particular transformation chosen -- is abstract.
Consequently, there are few restrictions on the further development
of the \DFD\ into a software design.
\item
The transformation is executable, which opens up possibilities for
automatically generating \VDM\ specifications from \DFDs. In this way,
the initial effort needed to produce a formal specification is
significantly decreased.
\item
The \DFDs\ and their \VDM\ counterparts can be regarded as equivalent
views on the system, using different representations.
\end{itemize}
A few restrictions apply to our transformation, however.
One of these is the exclusion of concurrent systems,
whereas some \SA\ extensions provide facilities for specifying such
systems.
We briefly mentioned how some of the \DFD\ constructs would be interpreted
if we had taken concurrency into account.
A transformation from a real-time \SA\ variant to a combination of \VDM\ and
e.g. CCS \cite{Milner80}, CSP \cite{Hoare85} or Petri nets \cite{Peterson77}
would be an interesting area for future research. We foresee that
the main problem in automatically providing a concurrent specification
description would be that such a description would have a very low level of
abstraction.
Intuitively it would be expected that each data transformer is transformed into
a {\em process} and that all these processes are executed in parallel. This
would result in a large number of processes due to the number of data
transformers usually present in a \DFD.
Concerns might also arise with respect to the size of the class of \DFDs\
having no cyclic internal data flows and obeying the one-to-one mapping
from input values to output values.
In our experience, cyclic data flows are often used to
model error situations which could also have been modeled by means of state
components in data stores. Therefore, most \DFDs\ with such cyclic
structures can be rewritten using only acyclic structures, and
therefore we believe that this restriction is not very important.
With respect to the restriction to one-to-one mappings between input
values and output values, we can say that usually the need for other
mappings only occurs when \DFDs\ are used as a design notation, but not
when they are used as an (abstract) specification notation. Therefore,
this restriction cannot be considered very important in our situation.
\newpage
\bibliographystyle{nnewalpha}
%% note: retrieve dan.bib from https://github.com/overturetool/overture/tree/development/documentation/bib
\bibliography{dan}
\appendix
\newpage
\section{Abstract Syntax for Structured Analysis}
The version of Structured Analysis considered in this \documenttype\
consists of a hierarchy of data
flow diagrams ($HDFD$), a data dictionary ($DD$), and a collection of
uniquely identified mini-specifications ($MSs$). The types of all data flows
in the data flow diagrams must be defined in the data
dictionary. In addition to this,
the signature of the top-level DFD must conform to
its topology.
\begin{vdm_al}
types
SA = HDFD * DD * MSs
inv mk_(hdfd,dd,-) ==
FlowTypeDefined(hdfd,dd) and TopLevelSigOK(hdfd);
\end{vdm_al}
The hierarchy of data flow diagrams is defined recursively. Each
$HDFD$ has a name, an unordered collection of data stores used in
the DFD, a description of its topology, a collection of
uniquely identified data transformers (``bubbles")
which are further decomposed as $HDFD$s,
and a description of the signatures of all the data transformers.
The invariant for $HDFD$ ensures that the signatures of the data
transformers (and the DFD as a whole) are consistent with the topology
and the data stores, and that all the DFDs which are further
decomposed are described.
\begin{vdm_al}
HDFD = DFDId * DSs * DFDTopo * DFDMap * DFDSig;
-- inv mk_(id,dss,dfdtop,dfdmap,dfdsig) ==
-- DFDSigConsistent(id,dfdtop,dss,dfdmap,dfdsig) and
-- LowerLevelUsed(dfdtop,dfdmap);
DSs = set of DSId;
DSId :: seq of char;
\end{vdm_al}
The topology of a DFD is a collection of uniquely identified data
flows. Each data flow is directed from a data transformer to another
data transformer. The data transformers can either be further decomposed
($DFDId$) or they can be primitive ($MSId$). An external process
($EPId$) is identified by its name.
At lower level DFDs where the data flow goes to (or comes
from) another data transformer which is outside the DFD the name is
omitted (the value {\textbf{\ttfamily nil}} is used).
The invariant requires that the topology of the
internal connections is acyclic.
\begin{vdm_al}
DFDTopo = map FlowId to ([ProcId] * [ProcId])
inv dfdtopo ==
let top={mk_(fid,tid)
|mk_(fid,tid) in set rng dfdtopo
& (is_DFDId(fid) or is_MSId(fid)) and
(is_DFDId(tid) or is_MSId(tid))} in
NotRecursive(top) and
forall flowid in set dom dfdtopo &
FlowConnectOK(dfdtopo(flowid));
FlowId = seq of char;
ProcId = DFDId|MSId|EPId;
DFDMap = map DFDId to HDFD;
DFDSig = map (DFDId|MSId) to Signature;
\end{vdm_al}
A signature for a description of a data transformer consists of
input, output, and state information. If a data transformer does not
have any connection to a state component which it is changing, it must produce
some output value instead.
\begin{vdm_al}
Signature = Input * Output * State
inv mk_(-,out,sta) ==
(sta=[]) => (out<>[]) and
(out=[]) => (exists mk_(-,m) in seq sta & m=<READWRITE>);
Input = seq of FlowId;
Output = seq of FlowId;
\end{vdm_al}
The {\em State} part of a signature is a sequence of pairs of state
variable identifiers (either data store identifiers or
data flows between the system and the external
processes) and the modes in which they are accessed.
\begin{vdm_al}
State = seq of (StId * Mode);
StId = DSId|FlowId;
Mode = <READ>|<READWRITE>;
DD = map Id to Type;
MSs = map MSId to MS;
MS = OpDef;
DFDId :: seq of char;
EPId :: seq of char;
MSId :: seq of char
\end{vdm_al}
\subsubsection*{Auxiliary Functions for Invariants}
All data flows must have a type defined in the data dictionary
(checked by $FlowTypeDefined$).
\begin{vdm_al}
functions
FlowTypeDefined : HDFD * DD -> bool
FlowTypeDefined(mk_(-,-,dfdtop,-,-),dd) ==
forall fid in set dom dfdtop &
FlowIdTypeConf(fid) in set dom dd;
\end{vdm_al}
The data flows between the external processes and
the specified system are treated as state components.
Therefore, the top-level
operation specifying the whole system contains no input or output
(checked by $TopLevelSigOK$).
All data flows must be present in the state component being either read or
write components, depending upon whether they are ingoing or outgoing data
flows.
\begin{vdm_al}
TopLevelSigOK: HDFD -> bool
TopLevelSigOK(mk_(sysid,-,dfdtop,-,dfdsig)) ==
sysid in set dom dfdsig and
let mk_(din,out,dst)=dfdsig(sysid) in
din=[] and out=[] and
forall flowid in set dom dfdtop&
let mk_(fid,tid)=dfdtop(flowid) in
(is_EPId(fid) =>
mk_(flowid,<READ>) in set elems dst) and
(is_EPId(tid) =>
mk_(flowid,<READWRITE>) in set elems dst);
\end{vdm_al}
In order for the signature mapping to be consistent it is necessary
to ensure that all data stores are connected to data transformers,
that all signatures reflect the information about flows from the
topology, that all identifiers mentioned in the signatures are
available, and finally that signatures are provided for all data
transformers used in the DFD (checked by $DFDSigConsistent$ and its
auxiliary functions).
\begin{vdm_al}
DFDSigConsistent: DFDId * DFDTopo * DSs * DFDMap * DFDSig
-> bool
DFDSigConsistent(id,dfdtop,dss,dfdmap,dfdsig) ==
DSConnected(dss,dfdsig) and
SigsAllRight(dfdtop,dfdsig) and
IdsInSigsAvail(dss,dfdtop, rng dfdsig) and
SigsForAllUsedIds(id, rng dfdtop,dfdmap,dfdsig);
DSConnected : DSs * DFDSig -> bool
DSConnected(dss,dfdsig) ==
forall dsid in set dss&
exists mk_(-,-,dst) in set rng dfdsig&
exists i in seq dst&
let mk_(id,-)=i in
dsid=id;
SigsAllRight : DFDTopo * DFDSig -> bool
SigsAllRight(dfdtop,dfdsig) ==
forall flowid in set dom dfdtop &
cases dfdtop(flowid):
mk_(id,mk_EPId(-)) -> let mk_(-,-,dst)=dfdsig(id) in
mk_(flowid,<READWRITE>) in set
elems dst,
mk_(mk_EPId(-),id) -> let mk_(-,-,dst)=dfdsig(id) in
mk_(flowid,<READ>) in set
elems dst,
mk_(nil, id) -> let mk_(din,-,-) = dfdsig(id)
in
flowid in set elems din,
mk_(id, nil) -> let mk_(-,out,-) = dfdsig(id) in
flowid in set elems out,
mk_(fid,tid) -> let mk_(-,out,-) = dfdsig(fid),
mk_(din,-,-) = dfdsig(tid) in
(flowid in set elems out) and
(flowid in set elems din)
end;
IdsInSigsAvail : DSs * DFDTopo * set of Signature -> bool
IdsInSigsAvail(dss,dfdtop,sigs) ==
let fids=CollectExtDFs(dfdtop) in
forall mk_(din,out,dst) in set sigs&
elems din subset dom dfdtop and
elems out subset dom dfdtop and
elems dst subset {mk_(id,m)
|id in set dss union fids,
m in set {<READ>,<READWRITE>}};
LowerLevelUsed : DFDTopo * DFDMap -> bool
LowerLevelUsed(dfdtop,dfdmap) ==
let ids = dom dfdmap in
forall mk_(fid,tid) in set rng dfdtop &
(is_DFDId(fid) => fid in set ids) and
(is_DFDId(tid) => tid in set ids);
SigsForAllUsedIds: DFDId * set of ([ProcId] * [ProcId]) *
DFDMap * DFDSig -> bool
SigsForAllUsedIds(id,top,dfdmap,dfdsig) ==
(forall dfdid in set dom dfdmap&
let mk_(-,-,-,-,dfdsig')=dfdmap(dfdid) in
dfdsig'(dfdid)=dfdsig(dfdid)) and
let sigs= dom dfdsig in
id in set sigs and -- dfds subset sigs and
forall mk_(fid,tid) in set top&
((is_MSId(fid) or is_DFDId(fid)) =>
(fid in set sigs)) and
((is_MSId(tid) or is_DFDId(tid)) =>
(tid in set sigs));
FlowConnectOK : ([ProcId] * [ProcId]) -> bool
FlowConnectOK(mk_(fid,tid)) ==
((is_EPId(fid) or fid=nil ) =>
(is_DFDId(tid) or is_MSId(tid))) and
((is_EPId(tid) or tid=nil ) =>
(is_DFDId(fid) or is_MSId(fid)));
NotRecursive : set of ((DFDId|MSId) * (DFDId|MSId)) ->
bool
NotRecursive(top) ==
forall mk_(f,-) in set top&
(f not in set TransClosure(f,top,{}));
TransClosure: (DFDId|MSId) * set of ((DFDId|MSId) *
(DFDId|MSId)) *
set of (DFDId|MSId) -> set of (DFDId|MSId)
TransClosure(pid,top,dset) ==
if exists mk_(fromid,toid) in set top&
((fromid=pid) or (fromid in set dset)) and
(toid not in set dset)
then let mk_(fromid,toid) in set top be st
((fromid=pid) or (fromid in set dset)) and
(toid not in set dset)
in TransClosure(pid,top,dset union {toid})
else dset
\end{vdm_al}
\newpage
\section{The Abstract Syntax for VDM-SL}
In this appendix we provide an abstract syntax for the part of VDM-SL
which we actually use in the definition of the formal semantics of
DFDs. The abstract syntax for the structuring part is an extension to
the abstract syntax from the VDM-SL standard because structuring is
not yet a part of the standard. However, this abstract syntax
correspond closely to a part of the abstract syntax used in the IFAD
VDM-SL language. The abstract syntax for the flat language is simply a
subset of the one used in the VDM-SL standard. None of the subsections
below are annotated because this is done elsewhere already.
\subsection{Abstract Syntax for Structuring}
\begin{vdm_al}
types
Document = set of Module;
Module = ModuleId * Interface * Definitions;
ModuleId = seq of char;
Interface = Imports * Export;
Imports = set of Import;
Import = ModuleId * ModuleSig;
Export = ModuleSig;
ModuleSig = set of Sig;
Sig = TypeSig|OpSig;
TypeSig :: TypeId;
TypeId = seq of char;
OpSig :: id: Id
optype : OpType
stids : seq of Id;
\end{vdm_al}
\subsection{Abstract Syntax for the Flat Language}
\begin{vdm_al}
Definitions = set of Definition;
Definition = StateDef|OpDef; --|...
StateDef :: id:Id
fields: seq of Field;
Field :: sel:[Id]
type:Type;
OpDef = ExplOp|ImplOp;
ExplOp :: id:Id
optype:OpType
parms: seq of Pattern
body:Stmt
dpre:Expr;
ImplOp :: id:Id
partp: seq of ParType
residtp:[IdType]
dext: seq of ExtVarInf
body:ImplOpBody;
ImplOpBody :: dpre:[Expr]
dpost:Expr;
ParType :: pat:Pattern
type:Type;
IdType :: id:Id
type:Type;
ExtVarInf :: mode:ReadWriteMode
id:Id
type:Type;
ReadWriteMode = <READ>|<READWRITE>;
OpType :: dom':[Type]
--> --------------------
--> maximum size reached
--> --------------------
