Check: http://checkstyle.sourceforge.net/config_javadoc.html#JavadocMethod

When programming in Java with JML annotations (http://www.jmlspecs.org/), the typical convention is to place the JML annotations - which are, for the purposes of any non-JML-aware tools, specially formatted Java comments - directly above the method they are annotating.

A Javadoc comment also needs to be placed above the method it is documenting. Most Javadoc processing tools (including "javadoc" itself with the standard doclet) have no problem ignoring non-Javadoc comments that occur between the Javadoc comment for a method and the method declaration. However, Checkstyle will fail to detect the Javadoc comment for a method if there is a multi-line (but not a single-line) comment between the Javadoc comment and the method declaration. For example, Checkstyle correctly detects the Javadoc in this case:

/**
 * A Javadoc comment.
 */
//@ A JML Annotation
public void foo() {}

but not in this case:

/**
 * A Javadoc comment.
 */
/*@ A JML Annotation */
public void foo() {} 

It would be very helpful for Checkstyle to be able to detect such Javadoc comments.

Examples of JML JavaDoc: https://sourceforge.net/apps/trac/jmlspecs/browser/TeachingMaterials/trunk/CAV2007Tutorial/examples/Actor.java?rev=2675 (https://sourceforge.net/apps/trac/jmlspecs/wiki/TeachingMaterials)

This change impacts the following checks:
UnusedImports
JavadocMethod
JavadocStyle
JavadocType
JavadocVariable
MissingJavadocMethod
MissingJavadocType
WriteTag