JML is a formal behavioral interface specification language for Java as documented in Design Contract With JML linked to from the University of Central Florida JML homepage. I read just the first half of the paper.