|
JML | ||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||||
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 | |
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 | ||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||||