In the Java course I'm currently doing at university, a lot of emphasis is placed on using JML constructs like @require and @ensure clauses in Javadoc comments. I understand that this is implementing the design by contract paradigm and that certain tools exist that are capable of mathematical verification of software using JML (assuming these clauses are defined appropriately).

I'm curious as to their prevalence in industry though. Are these clauses actually used? If so, how widely? It seems to me at least that enogh defensive programming can often make them redundant for trivial methods (even simple things like implementing null guards in the code).


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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.