JML

Package org.jmlspecs.samples.list

This package contains samples of JML specifications that are related to lists of various flavors.

See:
          Description

Class Summary
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.list Description

This package contains samples of JML specifications that are related to lists of various flavors. This package was written by and is maintained by Clyde Ruby. The purpose of these examples is to test some of the techniques developed in Clyde Ruby's dissertation research. Thus the programs are sometimes more complex than necessary. That is, the programs are not always typical or "ideal" ways to implement these classes, but rather serve to provide examples of how to deal with (when possible) some of the problems caused by aliasing and downcalls.


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.