---

solves-information-flow(es;T;S;F;In;X;f) ==
  (E(In) r E(X))
   es-interface-locs-list(es;X;S)
   (e:E(X)
       ((((f e) = e  e  In)  ((e  In)  (X(e) = In(e))))
        ((((f e) = e))
          (information-flow-relation(es;X;F;f e;loc(e))
             (X(e) = information-flow-to(es;X;F;f e;loc(e)))))))
   (e:E(X). i:Id.
       ((i  S)
        information-flow-relation(es;X;F;e;i)
        (e':E(X). ((loc(e') = i)  ((f e') = e)  ((e' = e))))))

---

Definitions :  subtype_rel: A r B,  es-interface-locs-list: es-interface-locs-list(es;X;S),  iff: P  Q,  assert: b,  in-eclass: e  X,  eclass-val: X(e),  information-flow-to: information-flow-to(es;X;F;e;i),  all: x:A. B[x],  l_member: (x  l),  implies: P  Q,  information-flow-relation: information-flow-relation(es;X;F;e;i),  exists: x:A. B[x],  Id: Id,  es-loc: loc(e),  and: P  Q,  apply: f a,  not: A,  equal: s = t,  es-E-interface: E(X)
FDL editor aliases :  solves-information-flow

---

solves-information-flow(es;T;S;F;In;X;f)  ==
    (E(In)  \msubseteq{}r  E(X))
    \mwedge{}  es-interface-locs-list(es;X;S)
    \mwedge{}  (\mforall{}e:E(X)
              ((((f  e)  =  e  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  In)  \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  In)  {}\mRightarrow{}  (X(e)  =  In(e))))
              \mwedge{}  ((\mneg{}((f  e)  =  e))
                  {}\mRightarrow{}  (information-flow-relation(es;X;F;f  e;loc(e))
                        \mwedge{}  (X(e)  =  information-flow-to(es;X;F;f  e;loc(e)))))))
    \mwedge{}  (\mforall{}e:E(X).  \mforall{}i:Id.
              ((i  \mmember{}  S)
              {}\mRightarrow{}  information-flow-relation(es;X;F;e;i)
              {}\mRightarrow{}  (\mexists{}e':E(X).  ((loc(e')  =  i)  \mwedge{}  ((f  e')  =  e)  \mwedge{}  (\mneg{}(e'  =  e))))))


Date html generated: 2010_08_27-PM-02_25_55
Last ObjectModification: 2010_01_26-PM-07_29_11

Home Index