[shawnjgoff]

Okay, I really don't understand this part: while (q) {G;} If p is true before the loop, then it must be true after the loop unless your loop has a break.

What if the condition p is that var_p == 1. And in the loop you decrement var_p. If the condition was true before the loop, it certainly is not if the loop ever runs.

[lucumo]

In the Wikipedia article it's shown a little bit more formally. It's basically: if you have a block G with the properties that {P ∧ Q} G {P}, you can create a while-loop with the properties that {P ∧ Q} while Q do G end {P ∧ ¬Q}.

(In a C like language, if holds:

  assert (P && Q);
  G ();
  assert (P);

then:

  assert (P && Q);
  while (Q) {
    G ();
  }
  assert (P && !Q);

also holds.)

Your misunderstanding is based on forgetting the conditions set for G. In your example, you will have a block G for which holds that before its execution var_p == 1 and that the same holds after its execution. From there it's probably easy to see that the same holds for while Q do G end. Since G doesn't change var_p, and Q is just a predicate without side effects, and the while itself doesn't change variables, var_p must be unchanged.

I hope I explained it clearly. I've been ready for bed for the past three hours or so, just can't drag myself to it :-)