JML

Package org.jmlspecs.samples.reader

This package contains samples of JML specifications relating to some abstractions of input and output.

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  
 

Package org.jmlspecs.samples.reader Description

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

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.