This package contains packages with samples of JML specifications. Its intent is mostly educational. The types contained in the packages beneath this one are not used directly in JML's implementation. However, they are used during testing of the implementation, and some of them are used in the various documents. Contributions are welcome.

All of the files in the subpackages check and pass the JML checker. They should all be able to be compiled with jmlc also, except that the dirobserver directory has specifications that are not (currently) executable. Aside from dirobserver, all the other subpackages have JML/JUnit tests that pass, and can also be seen as examples of that form of testing.