|
JML | ||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||||
See:
Description
| Interface Summary | |
| Reader | Readers. |
| Class Summary | |
| BlankReader | A reader that delivers a stream of blanks. |
| BlankReader_JML_Test | Automatically-generated test driver for JML and JUnit based testing of BlankReader. |
| BlankReader_JML_Test.OneTest | A JUnit test object that can run a single test method. |
| BlankReader_JML_Test.TestBlankReader | Test for the BlankReader contructor. |
| BlankReader_JML_Test.TestClose | Test for the close method. |
| BlankReader_JML_Test.TestRead | Test for the read method. |
| BlankReader_JML_Test.TestRefill | Test for the refill method. |
| BlankReader_JML_TestData | Supply test data for the JML and JUnit based testing of BlankReader. |
| BufferedReader | Buffered readers. |
| ReaderTest | Tests for the readers example. |
| 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 | |
This package contains samples of JML specifications relating to some abstractions of input and output. These samples were originally written by Arnd Poetzsch-Heffter, based on an example by K. Rustan M. Leino and Greg Nelson, that appears in their paper "Data abstraction and information hiding" (ACM Transactions on Programming Languages and Systems, volume 24, number 5, pp. 491-553, September 2002).
|
JML | ||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||||