Design by Contract is not commonly done, so such annotations would be quite uncommon. This doesn't mean they wouldn't be used at all! Instead, Design by Contract is most useful when correctness is of utmost importance, e.g. for algorithm implementation or safety-critical systems.
But the vast majority of software development is not considered safety-critical. Your requirements are more likely going to be “As a business analyst, I can click on a button to save the report as an Excel spreadsheet, so that I can perform my own analysis”. Formal verification adds no value under these circumstances, and it would be difficult to express useful contracts that can be verified.
The current industry best practice is to use automated test cases to verify that requirements are met and that systems behave correctly. Tests suffer from systematic limitations: tests are only examples and can't prove correctness for all inputs, unless I test all inputs. Tests and formal verification methods therefore don't replace each other, but complement each other: ideally, you do both.
The only automated formal verification system that is commonly used is the static type system of your programming language. Static typing can be used to express some simple contracts, though there are noticeable limitations, depending on the language. But even static typing is not used universally: plenty of significant development (even for security-sensitive systems such as web applications) happens in dynamic languages such as PHP, Python, or Ruby, that generally lack any kind of built-in static analysis.