Uses of Class
org.jmlspecs.samples.prelimdesign.USMoney_JML_Test.OneTest

Packages that use USMoney_JML_Test.OneTest

org.jmlspecs.samples.prelimdesign

This package contains samples of JML specifications from the paper Preliminary Design of JML.

Uses of USMoney_JML_Test.OneTest in org.jmlspecs.samples.prelimdesign

Subclasses of USMoney_JML_Test.OneTest in org.jmlspecs.samples.prelimdesign

protected static class	USMoney_JML_Test.TestCents Test for the cents method.
protected static class	USMoney_JML_Test.TestClone Test for the clone method.
protected static class	USMoney_JML_Test.TestDollars Test for the dollars method.
protected static class	USMoney_JML_Test.TestEquals Test for the equals method.
protected static class	USMoney_JML_Test.TestGreaterThan Test for the greaterThan method.
protected static class	USMoney_JML_Test.TestGreaterThanOrEqualTo Test for the greaterThanOrEqualTo method.
protected static class	USMoney_JML_Test.TestHashCode Test for the hashCode method.
protected static class	USMoney_JML_Test.TestLessThan Test for the lessThan method.
protected static class	USMoney_JML_Test.TestLessThanOrEqualTo Test for the lessThanOrEqualTo method.
protected static class	USMoney_JML_Test.TestMinus Test for the minus method.
protected static class	USMoney_JML_Test.TestPlus Test for the plus method.
protected static class	USMoney_JML_Test.TestScaleBy Test for the scaleBy method.
protected static class	USMoney_JML_Test.TestToString Test for the toString method.
protected static class	USMoney_JML_Test.TestUSMoney Test for the USMoney contructor.
protected static class	USMoney_JML_Test.TestUSMoney$1 Test for the USMoney contructor.