JML

Package org.jmlspecs.samples.dbc

This package contains samples of JML specifications written in the style of design by contract.

See:
          Description

Interface Summary
Complex Complex numbers.
 

Class Summary
Complex_JML_TestData Supply test data for the JML and JUnit based testing of Complex.
ComplexOps An abstract class that holds all of the common algorithms for complex numbers.
ComplexTest Test for the complex number types.
Polar Complex numbers in polar coordinates.
Rectangular Complex numbers in rectangular coordinates.
 

Package org.jmlspecs.samples.dbc Description

This package contains samples of JML specifications written in the style of design by contract. The ideas to demonstrate how JML can be used as a design by contract language. That is, of the specifications do not use JML's heavyweight specification cases, they did not use assignable clauses, and they mostly did not use model features. (There are however, a few model methods.)

The style of specification used in these examples leads to underspecification for interfaces. The solution would be to use model fields, however we do not wish to do that in this set of examples.


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.