NDBSL

Author: Rich Bradford

The Non-programmer database system (NDB) is a nicely engineered binary relational database system invented by Norman Winterbottom of IBM. The formal Specification of NDB was originally undertaken by Anne Walshe, who has subsequently documented the specification and its refinement. NDB has been used as an example problem for modular specification in VDM-SL. However, the version available here is a “flat” specification. The postscript file includes a significant description of the validation of the specification using execution. Test coverage is not used though. Relevant publications are:

A. Walshe, “NDB: The Formal Specification and Rigorous Design of a Single-User Database System”, in C.B. Jones and R.C. Shaw (eds), “Case Studies in Systematic Software Development”, Prentice Hall 1990, ISBN 0-13-116088-5

J.S. Fitzgerald and C.B. Jones, “Modularizing the Formal Description of a Database System”, in D. Bjorner, C.A.R. Hoare and H. Langmaack (eds), VDM ‘90: VDM and Z - Formal Methods in Software Development, Springer-Verlag, LNCS 428, 1990

Properties	Values
Language Version:	classic

ndb.vdmsl

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}

Overture Tool

Formal Modelling in VDM

NDBSL

ndb.vdmsl