What? The loop invariants aren't part of the spec! The loop invariants are just an intermediate step in your proof that the preconditions are enough to guarante

What? The loop invariants aren't part of the spec! The loop invariants are just an intermediate step in your proof that the preconditions are enough to guarantee that the postconditions will hold. If I was proving that 0 + 1 + .. n = n(n+1)/2, I wouldn't say that whatever induction step I chose to use was "part of the theorem", would I?