Quelle express.vdmsl Sprache: VDM

\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}

quality90%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.