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.
The source code for this package uses the GNU Lesser General Public License, since it is part of the JML runtime libraries.
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.