JML

Package org.jmlspecs.samples.jmlkluwer

This package contains samples of JML specifications from the paper "JML: a Notation for Detailed Design".

See:
          Description

Interface Summary
PriorityQueueUser  
 

Class Summary
PriorityQueue  
PriorityQueue_JML_Test Automatically-generated test driver for JML and JUnit based testing of PriorityQueue.
PriorityQueue_JML_Test.OneTest A JUnit test object that can run a single test method.
PriorityQueue_JML_Test.TestAddEntry Test for the addEntry method.
PriorityQueue_JML_Test.TestContains Test for the contains method.
PriorityQueue_JML_Test.TestIsEmpty Test for the isEmpty method.
PriorityQueue_JML_Test.TestNext Test for the next method.
PriorityQueue_JML_Test.TestPriorityQueue Test for the PriorityQueue contructor.
PriorityQueue_JML_Test.TestRemove Test for the remove method.
PriorityQueue_JML_Test.TestToString Test for the toString method.
PriorityQueue_JML_TestData Supply test data for the JML and JUnit based testing of PriorityQueue.
QueueEntry  
QueueEntry_JML_Test Automatically-generated test driver for JML and JUnit based testing of QueueEntry.
QueueEntry_JML_Test.OneTest A JUnit test object that can run a single test method.
QueueEntry_JML_Test.TestClone Test for the clone method.
QueueEntry_JML_Test.TestEquals Test for the equals method.
QueueEntry_JML_Test.TestGetLevel Test for the getLevel method.
QueueEntry_JML_Test.TestGetObj Test for the getObj method.
QueueEntry_JML_Test.TestHashCode Test for the hashCode method.
QueueEntry_JML_Test.TestQueueEntry Test for the QueueEntry contructor.
QueueEntry_JML_Test.TestToString Test for the toString method.
QueueEntry_JML_TestData Supply test data for the JML and JUnit based testing of QueueEntry.
TestSuite This class is automatically generated using org.multijava.util.testing.Main and is used to group a collection of JUnit tests for the local package and perhaps some subpackages.
TestSuite.TestSuite$1  
 

Exception Summary
PQException  
 

Package org.jmlspecs.samples.jmlkluwer Description

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.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.