Has anyone had success (or failure) in the real world with enforcing preconditions, postconditions and invariants? Has this caught bugs faster, reduced side effects and helped ensure overall correctness? Or has it lead to more overhead and longer development time without much to show for all the effort?