Does anybody write design-by-contract JavaDocs in the real world?

I'm conducting an informal, unscientific survey.  See the example below that I found recently. Does anybody outside of academia even do Design-by-Contract this way? I've been developing in Java since 2001 and I've never done it.  This is just too much work and I think I can safely bet that there are far more developers who are NOT familiar with these notations than those who are, thus making the method impractical for typical enterprise development environments, IMO. Is it just me or is this just another example of how big of a gap there is between the theory being taught in schools and actual industry practice?

You can easily find where this example came from by searching for "design-by-contract javadoc @requires"

I've been writing Java since 2006. Never heard of them, never used them, not planning on starting now.

Did some more searches and found JML: http://www.eecs.ucf.edu/~leavens/JML//index.shtml

Again, I have never used this in all the time I've spent developing Java applications nor have I ever seen it any of the JavaDoc comments of the many open source projects I have used throughout the years. I can't imagine any client for whom I have worked in the past would be happy to pay developers to spend much time writing these kinds of comments. Neither can I think of any developers who I dislike enough to make them write such comments.

Never heard of it. Found this

The example precondition ensures that the argument f of function sqrt() is greater than or equal to zero. Clients who use that method are responsible for adhering to that precondition. If they don't, we as implementors of sqrt() are simply not responsible for the consequences.

Laughed a lot over that part in bold. Sounds like bureaucratic lingo to me.
Oh you got an exception? Its your fault for passing illegal values. I was too lazy to code in proper checks. Instead I wrote a javadoc comment.

Tim Cooke wrote:I've been writing Java since 2006. Never heard of them, never used them, not planning on starting now.

I sure hope not. This is the kind of thing that can drive developers to madness, literally.

Junilu Lacar wrote:
I sure hope not. This is the kind of thing that can drive developers to madness, literally.

You can bet the management is going to love it then. I have lost quite a bit of hair and mental peace over maven already!  

I can safely say I've never seen that, and I've worked in lots of places over the past 15 odd years.

I can (possibly) see that sort of thing in engineering/scientific environments, maybe, where your algorithms are fairly tightly defined.
But even then, I would have thought a regular text JavaDoc that simply said what the algorithm was would be enough.

Dave Tolls wrote:I can (possibly) see that sort of thing in engineering/scientific environments, maybe, where your algorithms are fairly tightly defined.
But even then, I would have thought a regular text JavaDoc that simply said what the algorithm was would be enough.

My thoughts exactly. Very few developers know how to write good JavaDocs, even in plain language, much less with that much formality and rigor.

I'm in the Uncle Bob camp when it comes to code comments. The fewer the better.

So often have I encountered code where the description presented in the comments / JavaDocs do not match the reality. The comments were true at some point in the past but since then the code function has changed but the comments neglected. What you are left with are misleading lies scattered all over your codebase.

Yes, there is a belief amongst academics that modelling languages are good things, even though there doesn't seem to be much evidence for it. Designing a new modelling language enables you to publish something. That modelling language may allow code creation from the model, with assertions and algorithms also defined from the model. Though I could have sworn Eclipse would create a Java® class from an XML diagram ten years ago
I always thought Design by Contract was a trademark of the Eiffel people (Bertrand Meyer). The vocabulary of those comments isn't consistent with the Java® style, but looks more like Eiffel syntax, with “require” and “ensure”.
TC is right that inaccurate comments are positively harmful. But if the details have changed, why did they publish the documentation comments in the first place? If they made the commitment in the comments about the functionality of the method, why did they change it? Or were they simply exposing implementation details in th documentation comments which they ought to have kept quiet about? Once you publish a specification as a documentation comment, you have committed yourself to keep to it until you die or deprecate the code. Exposing an algorithm as Random#next() does condemns you to stick with that algorithm, though that method does suggest that overriding methods can use a different algorithm.
Design by Contract is not new to Bertrand Meyer; it is an elaboration and expression of weakest predicate semantics (Edsger Dijkstra) and P{Q}R (Sir Tony Hoare: P{Q}R is called a Hoare Triplet). What Meyer introduced in Eiffel is the concept that the precondition which applies to the parameter is applied as an assertion at the beginning of the function and the postcondition is applies at the end of the function as an assertion, using the REQUIRE and ENSURE keywords. That converts the preconditions to something akin to a guard, by causing an exception to be thrown if either assertion is false. The same applies to the postcondition, though a lot of things I have seen in Eiffel after ENSURE look like overkill. Certainly the bit about the size of a List being one more after adding an element looks like overkill. Verifying that the new element is now the last element in the List might be better, but again probaby overkill.
You can see how it shou‍ld be done for sqrt here, and you aren't using that abomination of a datatype float That sqrt method shou‍ld have read similarly.
There is also misunderstanding about what a precondition is. A precondition is a predicate that must be fulfilled if the method is to work correctly, and iContract is right to say

If a precondition fails, a bug is in a software component's client.

The text that Junilu bolded is correct; such errors are the responsibility of the client not the supplier. If as in the iContract example, it is a true precondition, then the method does not have to work correctly if it is not fulfilled. It is allowed to behave arbitrarily, fail to terminate, return a nonsense value (like the NaN for passing a negative argument), throw an Exception or something else. The method cannot accept responsibility for an incorrect argument. The worst possible case is that damage is done to the integrity of the object causing its to breach its invariants, but that damage is not noticeable until an incorrect result is obtained later on. It is best practice to document what actions are taken in case of an incorrect argument, whether returning a nonsense value (as sqrt does, but see the cbrt method shown by scrolling down the link one method), taking no action, or throwing an Exception, as this constructor does.

The concepts behind the DbC comment style are correct, but the format is incorrect. There is a Java® code style format and there has been for a long time, and the javadoc tool requires that format, so you shouldn't change it. What the sqrt method I linked to says is that it will provide the correct square root, as close as possible, without all that nonsense about the error being < 0.001, provided the argument is a defined (=not NaN) double not less than zero. It also says what it does for arguments < 0.0. The Color constructor shows how you can ensure correct arguments with an exception. It also shows the use of an annotation to match an immutable class without setXXX methods and the Bean Pattern. It is impossible to try to get a blue brighter than bright by passing (0, 0, 0, 0xff00) instead of the correct (0, 0, 0, 0xff).

A few minutes ago, I wrote:. . . It is impossible to try to get a blue brighter than bright by passing (0, 0, 0, 0xff00) instead of the correct (0, 0, 0, 0xff).

When I was teaching preconditions postconditions and invariants, I found how you can create a Color instance with (0, 0, 0, 0xff00) and it comes out bright green. I told the students, “A pint of beer for the first person who tells me how I managed that.”
Needless to say, I didn't have to buy any beer. When I told Peter how I did it, he told me off for cheating. “Of course it's cheating. You don't think I can do that sort of thing without cheating, do you?”

The ideas of contracts, preconditions, postconditions and invariants are important and should be understood by students learning how to develop software systems. To me they are as important as learning about the commutative, associative, distributive, etc. properties of operations in math. It's the utility of requiring students to learn and use a specific notation that I question. If you look through the rest of the course material from which the example I gave came, you'll see that the notation plays a big part in the course and knowing it and being able to decipher it seems to be a critical factor in completing quite a few of the course requirements. I would have no problem with that if it were part of a more advanced course of study but this is a follow-up introductory course and I think focusing on the notation at this point is like focusing more on learning Latin in an introductory biology class instead of learning more about the principles of heredity and classification.

Campbell Ritchie wrote:

If a precondition fails, a bug is in a software component's client.

The text that Junilu bolded is correct;

That was Maneesh's doing

Design by Contract is not new ... The concepts behind the DbC comment style are correct, but the format is incorrect. There is a Java® code style format and there has been for a long time, and the javadoc tool requires that format, so you shouldn't change it.

This is spot on but I don't know if there are many academics who understand this.

I am still hopeful that I can get a conversation around this going with the folks who developed and are using that course material in their instruction. My biggest concern, however, is that those folks will become defensive and that tends to make having a true dialogue difficult. I'd welcome any suggestions on how to turn this into a fruitful conversation and guide it in a direction where there would be at least an openness to consider making some very necessary, IMO, adjustments.

If you dig even deeper into the course materials, you'll see that the Java code that enforces preconditions uses assert. We all know you shouldn't do that since you can't assume that assertions are on. This is another thing I find disturbing about what is being taught. It wouldn't be too bad if the concept of guard clauses and "fail fast" design philosophy were the focus but again, it's not. Instead, I see instructors who are trapped in an implementation-focused perspective who are pulling students into that trap with them. The principles and concepts behind the implementation are all but glossed over, neglected, or forgotten altogether.

Junilu Lacar wrote:If you dig even deeper into the course materials, you'll see that the Java code that enforces preconditions uses assert. . . .

My opinion of Elizabeth who taught me Java® continues to rise. She taught us about using assertions and pointed out they can be enabled and disabled. Assertions are for testing time in development; the assertive way to handle arguments which don't fulfil the preconditions at runtime is IllegalArgu‍mentException.
Junilu and I would appear to agree that the concepts are right, but there is a particular Java® style and notation which shoul‍d be followed.