next up previous
Next: Meta-properties Up: Formal Model of Traces, Previous: Events and Traces

Trace Properties and Refinement

A trace property is a proposition on traces
\begin{program*} \> \\ \> TraceProperty$_{\mbox{\small {E}}}$\ ==\\ \> \vert E\vert List {}\mrightarrow{} \mBbbP{} \end{program*}
The following is the definition of the refinement relation on trace properties. It is read ``property P refines property Q''.
\begin{program*} \> \\ \> P $\rhd$\ Q ==\\ \> \mforall{}tr:\vert E\vert List\\ \> ((P tr) {}\mRightarrow{} (Q tr)) \end{program*}
Every property refines property P $_{\mbox{\small {True}}}$ defined by
\begin{program*} \> \\ \> P$_{\mbox{\small {True}}}$\ tr == True \end{program*}
Here are three trace properties that we will need in the sequel.
\begin{program*} \> \\ \> Causal$_{\mbox{\small {E}}}$\ tr ==\\ \> \mforall{}i... ...} (\muparrow{}(tr[j] \\ \> =msg=$_{\mbox{\small {E}}}$\ tr[i]))) \end{program*}

\begin{program*} \> \\ \> No-dup-send$_{\mbox{\small {E}}}$\ tr ==\\ \> \mfora... ...mbox{\small {E}}}$\ tr[j]))\\ \> {}\mRightarrow{} (i\\ \> = j)) \end{program*}

\begin{program*} \> \\ \> No-dup-deliver$_{\mbox{\small {E}}}$\ tr ==\\ \> \mf... ...oc$_{\mbox{\small {E}}}$\ tr[j]))\\ \> {}\mRightarrow{} (i = j)) \end{program*}


Richard Eaton 2002-02-20