Trace Terminology

May and Must Analyses §1

To describe how an analysis errors, we describe an analysis as either a may analysis $A^{𝗆 𝖺 𝗒}$ or a must analysis $A^{𝗆 𝗎 𝗌 𝗍}$ .

A May analysis states, if there exist a trace in the trace system of program p, which statisifies Q, then a may analysis should say that it is possible.

\exists τ \in Sem (p) . Q (τ) ⟹ A_{Q}^{𝗆 𝖺 𝗒} (p)

Alternatively, and more usefull, if a true may analysis does not say a property $Q$ may happen in $p$ , then it cannot happen:

\neg A_{Q}^{𝗆 𝖺 𝗒} (p) ⟹ \forall τ \in Sem (p) . \neg Q (τ)

A Must analysis states that if a must analysis says $Q$ is satisified in $p$ , then it must be satisfied for all traces in the tracesystem of $p$ .

A_{Q}^{𝗆 𝗎 𝗌 𝗍} (p) ⟹ \forall τ \in Sem (p) . Q (τ)

Or, if there exist a trace in the tracesystem of $p$ which satisifies $Q$ , then no must analysis can say it happens.

\exists τ \in Sem (p) . \neg Q (τ) ⟹ \neg A_{Q}^{𝗆 𝗎 𝗌 𝗍} (p)

Not-Must and Not-May Analyses §2

The may and must analyses contain two kinds of information, if the property holds for all traces, and to what side we error.

To this end we also use the terminology of a not-must and not-may analysis. A not-must property is a propty which does not hold for at least one traces, and a not-may is a property which does not hold for all traces.