A good place to start with JML is the Design-by-Contract with JML (PDF) document.
The Universe Type System Quick-Reference is a good starting point for the Universe type system.
The source code for the above document can be found at the JML homepage.