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_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.
TestSuite.TestSuite$1

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.