This package contains samples of JML specifications written in the style of design by contract. The ideas to demonstrate how JML can be used as a design by contract language. That is, of the specifications do not use JML's heavyweight specification cases, they did not use assignable clauses, and they mostly did not use model features. (There are however, a few model methods.)

The style of specification used in these examples leads to underspecification for interfaces. The solution would be to use model fields, however we do not wish to do that in this set of examples.