The Java Modeling Language (JML)

http://www.cs.iastate.edu/~leavens/JML/index.shtml
形式手法のノウハウをJavaに生かせないか考えていたんだけれど、すでにこういうのがあった。どうやら、javadocみたいにコメントに事前条件、事後条件、不変条件などを書くみたい。静的検証ではなく動的検証の模様。