This paper argues that specified blocks have every advantage over the combination of assertions, preconditions, postconditions, invariants, and variants, both for verifying programs, and for program development. They are simpler, more general, easier to write, and they make proofs easier.
Eric C. R. Hehner