[sv-ac] Annex H change for 269

All:

A while ago I said that we should review how the
formal semantics in Annex H should (or should not)
change in response to the clarification of what
can appear in the reset expression of a "disable iff".

In Annex H, H.3.6.1, p. 551, we say that

   w,L_0 |= disable iff (b) P iff either w,L_0 |= P or
   there exists 0 <= k <= |w| such that w^k |= b[L_0] and
   w^{0,k-1}\top^\omega,L_0 |= P. Here w^{0,-1} denotes
   the empty word.

By looking for "w^k |= b[L_0]", we are saying that the
valuation of the local variables in L_0 affects the evaluation
of the reset expression b.

I think we should change "w^k |= b[L_0]" to "w^k |= b".

According to 269, there cannot be any local variables in
b. And if there are no local variables in b, then
"w^k |= b[L_0]" is equivalent to "w^k |= b". Thus, technically,
no change to Annex H is required.

However, by leaving the condition as "w^k |= b[L_0]", we are
confusing the reader of Annex H, who may reasonably think that
b can depend on local variables and that the local variable
values are used in evaluating b.

Best regards,

John H.
Received on Mon Nov 29 08:50:06 2004