Quellcodebibliothek ndb.vdmsl Sprache: 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}

quality94%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.