Package org.jmlspecs.samples.dbc

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


Interface Summary
Complex Complex numbers.

Class Summary
Complex_JML_Test Automatically-generated test driver for JML and JUnit based testing of Complex.
Complex_JML_Test.OneTest A JUnit test object that can run a single test method.
Complex_JML_Test.TestAdd Test for the add method.
Complex_JML_Test.TestAngle Test for the angle method.
Complex_JML_Test.TestDiv Test for the div method.
Complex_JML_Test.TestEquals Test for the equals method.
Complex_JML_Test.TestHashCode Test for the hashCode method.
Complex_JML_Test.TestImaginaryPart Test for the imaginaryPart method.
Complex_JML_Test.TestMagnitude Test for the magnitude method.
Complex_JML_Test.TestMul Test for the mul method.
Complex_JML_Test.TestRealPart Test for the realPart method.
Complex_JML_Test.TestSub Test for the sub method.
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.
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.

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 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.