|
\documentclass{article}
\usepackage{a4}
\usepackage{makeidx}
\usepackage{vdmsl-2e}
\newcommand{\StateDef}[1]{{\bf #1}}
\newcommand{\TypeDef}[1]{{\bf #1}}
\newcommand{\TypeOcc}[1]{{\it #1}}
\newcommand{\FuncDef}[1]{{\bf #1}}
\newcommand{\FuncOcc}[1]{#1}
\newcommand{\ModDef}[1]{{\tiny #1}}
\makeindex
\begin{document}
\title{Mapping between EXPRESS representations}
\author{Submitted by Marcel Verhoef}
\maketitle
\begin{vdm_al}
module Database
exports all
definitions
types
PhysicalFile ::
headersec : map seq of char to seq of Parameter
datasec : map nat to ([Scope] * Record);
HeaderEntity ::
name : seq of char
parms : seq of Parameter;
Scope :: ;
Record = SimpleRecord | SuperRecord ;
SuperRecord ::
rec_list : seq of SimpleRecord;
SimpleRecord ::
name : seq of char
parms : seq of Parameter;
Parameter = StringParameter |
RealParameter |
IntegerParameter |
EntityInstanceName |
EnumerationParameter |
BinaryParameter |
ListParameter |
TypedParameter |
OmittedParameter |
UnknownParameter ;
StringParameter ::
data : seq of char;
RealParameter ::
data : real;
IntegerParameter ::
data : int;
EntityInstanceName ::
data : nat;
EnumerationParameter ::
data : seq of char;
BinaryParameter ::
data : bool;
ListParameter ::
data : seq of Parameter;
TypedParameter::
name : seq of char
data : Parameter;
OmittedParameter:: ;
UnknownParameter::
operations
CheckReferences: Parameter ==> set of nat
CheckReferences(parm) ==
cases parm:
mk_EntityInstanceName(id) -> return {id},
mk_ListParameter(parms) ->
( dcl res : set of nat := {};
for subparm in parms do
res := res union CheckReferences(subparm);
return res),
others -> return {}
end;
FindAllReferencesToEntity: nat ==> set of nat
FindAllReferencesToEntity (eid) ==
let eins = dom in_model.datasec \ {eid}
in
( dcl res : set of nat := {};
for all ein in set eins do
let mk_(-,mk_SimpleRecord(-,parms)) =
in_model.datasec(ein)
in
if eid in set CheckReferences(
mk_ListParameter(parms))
then res := res union {ein};
return res
);
FindAllInstances: seq of char ==> set of nat
FindAllInstances(nm) ==
let eins = dom in_model.datasec
in
( dcl res : set of nat := {};
for all ein in set eins do
let mk_(-,rec) = in_model.datasec(ein)
in
if IsA (rec, nm)
then res := res union {ein};
return res
);
LookUpEntityInstance: nat ==> [Record]
LookUpEntityInstance (ein) ==
let eins = dom in_model.datasec
in
if ein in set eins
then let mk_(-,rec) = in_model.datasec(ein)
in
return rec
else return nil;
TransformRmVertex: nat ==> nat
TransformRmVertex(rmv_id) ==
let mk_SimpleRecord(-,parms) = LookUpEntityInstance (rmv_id)
in
let mk_EntityInstanceName(cpnt_id) = parms(5)
in
return cpnt_id;
TransformRmEdge: nat ==> set of (nat * nat)
TransformRmEdge (rme_id) ==
let mk_SimpleRecord(-,parms) = LookUpEntityInstance(rme_id)
in
let mk_ListParameter(rmees) = parms(3)
in
( dcl res : set of (nat * nat) := {};
for rmee in rmees do
let mk_EntityInstanceName(rmee_id) = rmee
in
let {rmee_ref} = FindAllReferencesToEntity(rmee_id)\{rme_id}
in
res := res union {mk_(rme_id, TransformRmVertex(rmee_ref))};
return res
);
TransformRmLoop: nat ==> seq of nat
TransformRmLoop (rml_id) ==
let mk_SimpleRecord(-,parms) = LookUpEntityInstance (rml_id) in
let mk_ListParameter(rmess) = parms(2) in
( dcl res : set of (nat * nat) := {};
for rmes in rmess do
let mk_EntityInstanceName(rmes_id) = rmes in
let rme_ref = FindAllReferencesToEntity(rmes_id) \ {rml_id} in
for all rme_id in set rme_ref do
res := res union TransformRmEdge(rme_id);
return SortPoints(res)
);
Transform: () ==> set of seq of nat
Transform () ==
let rmls = FindAllInstances("RM_LOOP") in
( dcl res : set of seq of nat := {};
for all rml in set rmls do
res := res union {TransformRmLoop(rml)};
return res
);
Create: set of seq of nat ==> ()
Create (AbstrMod) ==
( dcl ds : map nat to ([Scope] * Record) := {|->},
LookUpTable : map nat to nat := {|->},
polylist : seq of EntityInstanceName := [];
for all ent in set Collect(AbstrMod) do
( last_id := last_id + 1;
LookUpTable := LookUpTable munion { ent |-> last_id };
let mk_SimpleRecord(-,parms) = LookUpEntityInstance(ent) in
ds := ds munion { last_id |-> mk_(nil,
mk_SimpleRecord("VERTEX",[parms(3)]))}
);
for all poly in set AbstrMod do
( last_id := last_id + 1;
ds := ds munion { last_id |-> mk_(nil,
mk_SimpleRecord("POLYLINE",[mk_ListParameter(
MapInToOut(poly,LookUpTable))]))};
polylist := polylist ^ [mk_EntityInstanceName(last_id)]
);
ds := ds munion { last_id + 1 |-> mk_(nil,
mk_SimpleRecord("DRAWING",[mk_ListParameter(polylist)]))};
out_model := mk_PhysicalFile (
{ "FILE_NAME" |-> [mk_UnknownParameter()],
"FILE_DESCRIPTION" |-> [mk_UnknownParameter()],
"FILE_SCHEMA" |-> [mk_UnknownParameter()] }
, ds )
);
DoMapping: PhysicalFile ==> PhysicalFile
DoMapping (pf) ==
( in_model := pf;
Create(Transform());
return out_model
)
functions
MapInToOut : seq of nat * map nat to nat -> seq of EntityInstanceName
MapInToOut (ins, lut) ==
if ins = [] then
[]
else
[mk_EntityInstanceName(lut(hd ins))] ^ MapInToOut(tl ins, lut)
measure LenPar1;
LenPar1: seq of nat * map nat to nat -> nat
LenPar1(list,-) ==
len list;
Collect : set of seq of nat -> set of nat
Collect (theSet) ==
cases theSet:
{} -> {},
others -> let e in set theSet in elems e union Collect(theSet\{e})
end
measure SetCard;
SetCard: set of seq of nat -> nat
SetCard(s) ==
card s;
IsA: Record * seq of char -> bool
IsA(rec,nm) ==
if is_SimpleRecord(rec) then
let mk_SimpleRecord (name,-) = rec in
nm = name
else
false;
SortInnerLeft: set of (nat * nat) * nat -> seq of nat
SortInnerLeft (theSet, goal) ==
cases theSet:
{} -> [],
others ->
let mk_(a,b) in set theSet be st a = goal in
SortInnerRight(theSet\{mk_(a,b)}, b)
end;
SortInnerRight: set of (nat * nat) * nat -> seq of nat
SortInnerRight (theSet,goal) ==
cases theSet:
{} -> [],
others ->
let mk_(a,b) in set theSet be st b = goal in
[b] ^ SortInnerLeft(theSet\{mk_(a,b)}, a)
end;
SortPoints : set of (nat * nat) -> seq of nat
SortPoints (theSet) ==
let mk_(a,b) in set theSet in
SortInnerRight(theSet\{mk_(a,b)},b)
state Kernel of
in_model : PhysicalFile
out_model : PhysicalFile
last_id : nat
init
k == k = mk_Kernel(
mk_PhysicalFile({|->},{|->}),
mk_PhysicalFile({|->},{|->}),
0
)
end
end Database
\end{vdm_al}
\printindex
\end{document}
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.20Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
