| products/Sources/formale Sprachen/VDM/VDMSL/DFDexampleSL/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: coq_micromega.mli Sprache: VDMOriginal von: VDM© |
|
||||||
|
\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 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, 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, 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 \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/developm \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 --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.162Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
