This package contains samples of JML specifications from the paper "JML: a Notation for Detailed Design". This paper, by Gary T. Leavens, Albert L. Baker, and Clyde Ruby, appeared as chapter 12 of the book Behavioral Specifications for Businesses and Systems, Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors). (This book is copyright Kluwer Academic Publishers, 1999, and the chapter appears in the JML release by permission.)

These examples mostly have to do with priority queues.