Question

w denotes a non-empty finite or infinite word over Σ. Assume that all properties, sequences, and unclocked

property fragments do not involve local variables.

Neutral satisfaction of assertions:

For the definition of neutral satisfaction of assertions, b denotes the boolean expression representing the

enabling condition for the assertion. Intuitively, b is derived from the conditions in the context of a procedural

assertion, while b is “1” for a declarative assertion.

? w, b always @(c) assert property P iff for every 0 < i < |w| such that w i c and w i b,

w i.. @(c) P.

? w, b always assert property Q iff for every 0 < i < |w|, if w i b then w i.. Q .

? w, b initial @(c) assert property P iff for every 0 < i < |w| such that w 0, i !c [*0:$] ##1 c and

w i b, w i.. @(c) P .

? w, b initial assert property Q iff (if w 0 b then w Q ) .

Neutral satisfaction of properties:

? w ( P ) iff w P.

? w Q iff w Q’, where Q’ is the unclocked property that results from Q by applying the rewrite rules.

? w disable iff (b) P iff either w P or there exists 0 < k < |w| such that w k b and

w 0, k–1 Tω P. Here, w 0, –1 denotes the empty word.

? w not P iff w P.

? w R iff there exists 0 < j < |w| such that w 0, j R .

? w ( R |-> P ) iff for every 0 < j < |w| such that w 0, j R, w j.. P .

? w ( P1 or P2 ) iff w P1 or w P2.

? w ( P1 and P2 ) iff w P1 and w P2.

Remark: Since w is non-empty, it can be proved that w not b iff w !b.