I still can't see how you can infer that the assume(!running) which clearly holds after the loop also holds before the loop.
It holds if the loop does not change running, trivially? But then you no longer have a loop.Note also that you can implement an if construct from while this way:
while(B){
S;
B=false;
}
If that was the case, then you could not infer anything about B
before the while.
