I'm working on understanding the one-bit protocol in the "Principles" section of the hyperbook, and have a question about the following construction. The book says on page 10:
Doesn't this code allow the statement to be executed zero times, in particular, if the "or skip" is nondeterministically chosen? If so, can't we reach later code with x[self] having no value, in particular, no Boolean value? If so, doesn't that defeat the purpose of the construction, which is "... set x[self] to a Boolean..."