Consider the definition of formula b for the original
Session6 algorithm:
/\ pc = "b" /\ x' = x + (2*i - 1) /\ pc' = "a" /\ i' = iSuppose we deleted the conjunct
i' = i from this
formula. I've found that almost all programmers and software
engineers believe that should make no difference. They are used
to thinking in terms of programming languages, where the value of a
variable remains unchanged unless a statement explicitly changes
it. So, they think that the natural interpretation of a formula
describing a step is that the value of any variable not mentioned in
the formula must be unchanged by the step.
That's not a natural interpretation. Suppose I told you:
John and I ate at Luigi's Trattoria last night and I then went home to bed.Since I said nothing about what John did after dinner, does that mean he spent the night at the trattoria? No. You naturally know that there are lots of places John could have gone after dinner.
Math is based on the simple idea that a formula says
nothing about anything not mentioned in the
formula. Removing the last conjunct from the definition of
b allows steps in which i can have any
values in the starting and ending states. If you ran TLC after
removing that conjunct, it would raise an error (if N is
greater than 0) because after the first a step, there are
infinitely many possible b steps — something TLC
can't cope with.
In the modified algorithm, if the second conjunct of b
were
x'[i] = x[i-1] + (2*i - 1)then that formula would say something only about the value of
x[i] in a step's second state. It would say nothing
about the values of x[j] for the N values of
j in (0..N) \ {i}. In fact, it would
say nothing about what the domain of x is in the step's
second state. A translation of the PlusCal statement
b must describe the new value of x, not just
the new value of x[i].