[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 :-)