I first wrote the example that code as
int old_a2b = 0, old_b2a = 0 while old_a2b >= 0 and old_b2a >= 0 int new_a2b, new_b2a co { old_b2a >= 0 } new_a2b = f(old_b2a) old_a2b = new_a2b ... || { old_a2b >= 0 } new_b2a = g(old_a2b) old_b2a = new_b2a ... oc
This is manifestly stupid code, because, while the assignments into the new variables don't interfer with the preconditions, the assignments into the old variables do.
This page last modified on 11 June 2003.