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).
Industry Prevalence of JML Specification
java;design patterns;javadocs;industry standard