JML

Package org.jmlspecs.lang

This package is a collection of types used in the definition of the JML language.

See:
          Description

Interface Summary
JMLSetType Common protocol for the JML set model types.
 

Class Summary
JMLDataGroup A type with one element, for use in declaring "data groups".
JMLDataGroup_JML_Test Automatically-generated test driver for JML and JUnit based testing of JMLDataGroup.
JMLDataGroup_JML_Test.OneTest A JUnit test object that can run a single test method.
JMLDataGroup_JML_Test.TestClone Test for the clone method.
JMLDataGroup_JML_Test.TestEquals Test for the equals method.
JMLDataGroup_JML_Test.TestHashCode Test for the hashCode method.
JMLDataGroup_JML_Test.TestToString Test for the toString method.
JMLDataGroup_JML_TestData Supply test data for the JML and JUnit based testing of Person.
 

Package org.jmlspecs.lang Description

This package is a collection of types used in the definition of the JML language.

At present the only type in this package is JMLDataGroup. The type JMLDataGroup is useful for specifications that want to use Rustan Leino's notion of data groups. This type has exactly one non-null value. (That is, all non-null objects of the type are .equals to each other.) To declare the equivalent of a data group, declare a model value of this type and make it depend on all of the elements of the data group. Note that in JML, all public and protected fields also have an implicit data group associated with them.

Coding

The source code for this package uses the GNU Lesser General Public License, since it is part of the JML runtime libraries.

Acknowledgments

At Iowa State, the development of JML was partially funded by the (US) National Science Foundation under grants CCR-9503168, CCR-9803843, CCR-0097907, and CCR-0113181.


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.