products/Sources/formale Sprachen/VDM/VDMSL/NDBSL/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ndb.vdmsl   Sprache: VDM

Original von: VDM©
types

 Eid = token;
 Value = token; 
 Esetnm = token;
 Rnm = token;
 
 Maptp = <ONETOONE>|<ONETOMANY>|<MANYTOONE>|<MANYTOMANY>;

 Tuple :: fv : Eid
   tv : Eid;

 Rinf :: tp : Maptp
   r : set of Tuple;
   
 Rkey :: nm : [Rnm]
  fs : Esetnm
  ts : Esetnm

functions

checkinv : map Esetnm to set of Eid * map Eid to [Value] * map Rkey to
Rinf -> bool
checkinv (esm,em,rm) ==
dom em = dunion rng esm and
              forall rk in set dom rm &
                 let mk_Rkey(-,fs,ts)=rk in
                 let mk_Rinf(tp,r) = rm(rk) in
                        {fs,ts} subset dom esm and
                        (tp = <ONETOMANY> => forall t1,t2 in
                        set r & t1.tv = t2.tv  => t1.fv = t2.fv) and
                        (tp = <MANYTOONE> => forall t1,t2 in
                        set r & t1.fv = t2.fv =>t1.tv = t2.tv) and
                        (tp = <ONETOONE> => forall t1,t2 in
                        set r & t1.fv = t2.fv <=> t1.tv = t2.tv) and
                        forall mk_Tuple(fv,tv) in set r & fv
                        in set esm(fs) and tv in set esm(ts)



state Ndb of

  esm : map Esetnm to set of Eid
  em  : map Eid to [Value]
  rm  : map Rkey to Rinf

  inv mk_Ndb(esm,em,rm) == checkinv (esm,em,rm)

init  ndb == ndb = mk_Ndb({|->},{|->},{|->})
end

 operations

 
 ADDES(es:Esetnm)
 ext wr esm : map Esetnm to set of Eid
 pre es not in set dom esm
 post esm = esm~ munion {es |-> {}};

 DELES(es:Esetnm)
 ext wr esm : map Esetnm to set of Eid
     rd rm  : map Rkey to Rinf
 pre es in set dom esm and esm(es) = {} and
     es not in set {rk.fs | rk in set dom rm } union {rk.ts |
     rk in set dom rm}
 post esm = {es} <-: esm~;


 ADDENT(memb : set of Esetnm, val : [Value]) eid :Eid
 ext wr esm : map Esetnm to set of Eid
     wr em  : map Eid to [Value]
 pre memb subset dom esm
 post eid not in set dom em~ and
      em = em~ munion {eid |-> val} and
      esm = esm~ ++ {es |-> esm~(es) union {eid} | es in set
      memb };

 DELENT(eid:Eid)
 ext wr esm : map Esetnm to set of Eid
     wr em  : map Eid to [Value]
     rd rm  : map Rkey to Rinf
 pre eid in set dom em and
     forall t in set dunion{ri.r|ri in set rng rm}& t.fv <>
     eid and t.tv <> eid
 post esm = {es |-> esm~(es) \ {eid} | es in set dom esm~} and
      em = {eid} <-: em~;

 ADDREL( rk:Rkey, tp:Maptp)
 ext rd esm : map Esetnm to set of Eid
     wr rm  : map Rkey to Rinf
 pre {rk.fs,rk.ts} subset dom esm and
     rk not in set dom rm
 post rm = rm~ munion {rk |-> mk_Rinf(tp,{})};

 DELREL (rk:Rkey)
 ext wr rm : map Rkey to Rinf
 pre rk in set dom rm and (rm(rk)).r ={}
 post rm ={rk} <-:rm~;

 ADDTUP (fval,tval : Eid, rk:Rkey)
 ext wr rm  : map Rkey to Rinf
     rd esm : map Esetnm to set of Eid 
        rd em  : map Eid to [Value]
 pre rk in set dom rm and 
     let ri = mu(rm(rk),r |-> (rm(rk)).r union
     {mk_Tuple(fval,tval)}) in
  checkinv (esm,em,rm ++ {rk |->ri})
 post let ri =mu(rm~(rk),r |-> (rm~(rk)).r union
 {mk_Tuple(fval,tval)}) in rm =rm~ ++ {rk |->ri};

 DELTUP(fval,tval:Eid, rk:Rkey)
 ext wr rm : map Rkey to Rinf
 pre rk in set dom rm
 post let ri = mu(rm~(rk),r |-> (rm~(rk)).r \
      {mk_Tuple(fval,tval)}) in
      rm =rm~ ++ {rk |->ri}

¤ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff