> First, I'd love to see REQUIRE or some such added for "precondition" > non-null checks. That's mostly an aside, though. If I'm following what you mean, check out http://www.cs.ucf.edu/~leavens/JML/. sincerely.