EDIT: Actually, the original spec doesn't even say what is a valid state after initialization. It provides only a requirement on the initial state (that w + b > 0 and that w and b are both in Nat, or >= 0, when initialized). The correctly formulated rules ensure that w and b remain in Nat, but there's no other piece of the specification that seems to require it.
Once the author starts adding invariants (like NotEmpty) that adds a requirement that w + b > 0 remains true for ever, but since w is incremented and b is decremented, even BB results in NotEmpty remaining satisfied. Each of the steps does, since they all add one bean back.