This package contains samples of JML specifications from the paper Preliminary Design of JML. The idea is that otherwise uncategorized examples from the preliminary design document should appear here, so that they can be looked at independently and checked by the checker and our tests.