---

PropertyNR ==
  es:EO+(Info). n:E(New). e:E.
    ((loc(e) = loc(n))
     ((New(n) released before e))
     (e':E. (((loc(e') = loc(e)))  e' has* New(n)  (e < e'))))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  es-E-interface: E(X),  release-before: (a released before e),  all: x:A. B[x],  es-E: E,  not: A,  equal: s = t,  Id: Id,  es-loc: loc(e),  implies: P  Q,  event-has*: e has* a,  eclass-val: X(e),  ses-new: New,  es-causl: (e < e')
FDL editor aliases :  ses-NR

---

PropertyNR  ==
    \mforall{}es:EO+(Info).  \mforall{}n:E(New).  \mforall{}e:E.
        ((loc(e)  =  loc(n))
        {}\mRightarrow{}  (\mneg{}(New(n)  released  before  e))
        {}\mRightarrow{}  (\mforall{}e':E.  ((\mneg{}(loc(e')  =  loc(e)))  {}\mRightarrow{}  e'  has*  New(n)  {}\mRightarrow{}  (e  <  e'))))


Date html generated: 2010_08_28-AM-02_33_14
Last ObjectModification: 2010_02_22-PM-05_10_05

Home Index