Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/Sources/formale Sprachen/Isabelle/HOL/ex/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 20 kB image not shown  

SSL dfdexample.vdmsl   Interaktion und
PortierbarkeitVDM

 
\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 described.
\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

--> --------------------

84%


¤ Dauer der Verarbeitung: 0.73 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.





                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge