Java: Design by Contract annotations

Question

I've recently started to read up on the Design by Contract design method but I don't understand some aspects of it. When using @pre etc, in a javadoc style comment, what purpose do these tags serve other than as documentation? Does the compiler use these for checks on the parameters before execution, or are these just indicators as to what kind of checks should occur in the method? e.g. if i have a getAge method;

/**
* @pre age >= 0 #CustomAgeException
*/
public int getAge() throws CustomAgeException{
    return age;
}

Will this cause a check at runtime before running the method, Does the compiler check this, or does this simply state to the developer that age must be equal or greater than 0 before calling this method, and that a check should be performed within getAge?

score 3 · Answer 1 · answered Feb 16 '15 at 11:50

3

Java does not directly support Design by Contract. As Robin Jonsson said, JavaDoc is inaccessible at runtime.

However, there are different tools you could use such as JMSAssert which can access the annotations. For more details: http://www.mmsindia.com/JMSAssert.html

answered Feb 16 '15 at 11:50

DeiAndrei

947
6
16

From the JMSAssert webpage: "JMSAssert is currently available on Windows platforms only. JDK Versions supported: 1.2.0 to 1.3.1." – mernst Feb 20 '15 at 07:20

score 2 · Accepted Answer · edited May 23 '17 at 12:20

2

JavaDoc is inaccessible at runtime. The .class file doesn't contain them. (Reference see here StackOverflow question) Therefor, any code that would check for a javadoc is impossible.

The comment is simply to make beautiful javadoc, or to keep the same pattern for these kind of notes across the classes. You'd have to implement the check yourself, or use a framework of some kind to actually perform the check. (Perhaps with real annotations on method/parameter level)

Regards

edited May 23 '17 at 12:20

Community

1
1

answered Feb 16 '15 at 11:46

Robin Jonsson

2,761
3
22
42

ah ok so it exists solely as documentation for developers then? – jbailie1991 Feb 16 '15 at 11:50
@jbailie1991Yes as far as I can see – Robin Jonsson Feb 16 '15 at 13:37

score 2 · Answer 3 · answered Feb 19 '15 at 10:11

Specifications, such as design-by-contract annotations, document how your code is supposed to behave. This is useful as documentation, so that you can find bugs in your code and clients of your code can use it correctly.

It's even better to have machine-checked documentation so that you get a guarantee that your code is bug-free and clients are using it correctly. Run-time assertions can help with this, but they give no guarantee: they may fail at run time.

It's best for the compiler to check the specifications before execution, as you asked in your question. (Unfortunately, the other answers ignored this part of your question and focused on run-time checking.) There are various frameworks that will do compile-time checking of specifications. Because the problem is undecidable in general, all of the frameworks have limitations, but you might find them useful nonetheless. One good option is the Checker Framework, which lets you define type annotations such as @NonNegative, write them in your code, and the compiler verifies that your code is consistent with the annotations.

Java: Design by Contract annotations

3 Answers3