This package contains miscellaneous samples of JML specifications. Many of these are related to verification issues, and some are illustrating points about behavioral subtyping.