I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one shouldn't lead you to alter the first proof. But it does if you carelessly use some logical tools like dependent types and single preconditions/postconditions/loop invariants.
and, in order to prove another property, some new invariant Q has to be propagated across this loop. It would be enough to prove
{Q∧B}S{Q}
or even
{P∧Q∧B}S{Q}
if the new proof builds upon the first one. But if your logical tool of choice insists on having a unique loop invariant, you must throw away your existing proof and prove
{P∧Q∧B}S{P∧Q}
which is incomparable and uselessly mixes both concerns.
You don't have to edit ("throw away") your original proof, it's just that a single proof covering the most precise description of the program's behavior is more compact than restating the program code a bunch of times plus the additional ceremony to assert that all those proofs refer to the same program.
> a single proof covering the most precise description of the program's behavior is more compact
Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We have compilers with LTO for that, though; we would never maintain source code in that form.
Snark aside, I get your point about restating the program code, but this can be alleviated by interactive proof assistants that largely reduce the length of proof scripts. This is mostly a matter of tooling.
For example, take Hoare's while rule (see https://en.wikipedia.org/wiki/Hoare_logic#While_rule). If you have already proved
and, in order to prove another property, some new invariant Q has to be propagated across this loop. It would be enough to prove or even if the new proof builds upon the first one. But if your logical tool of choice insists on having a unique loop invariant, you must throw away your existing proof and prove which is incomparable and uselessly mixes both concerns.