|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use org.jmlspecs.samples.prelimdesign | |
| org.jmlspecs.samples.prelimdesign | This package contains samples of JML specifications from the paper Preliminary Design of JML. |
| Classes in org.jmlspecs.samples.prelimdesign used by org.jmlspecs.samples.prelimdesign | |
| Account
|
|
| Account_JML_Test
Automatically-generated test driver for JML and JUnit based testing of Account. |
|
| Account_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| Account_JML_TestData
Supply test data for the JML and JUnit based testing of Account. |
|
| IntMathOps2_JML_Test
Automatically-generated test driver for JML and JUnit based testing of IntMathOps2. |
|
| IntMathOps2_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| IntMathOps2_JML_TestData
Supply test data for the JML and JUnit based testing of IntMathOps2. |
|
| IntMathOps4_JML_Test
Automatically-generated test driver for JML and JUnit based testing of IntMathOps4. |
|
| IntMathOps4_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| IntMathOps4_JML_TestData
Supply test data for the JML and JUnit based testing of IntMathOps4. |
|
| IntMathOps_JML_Test
Automatically-generated test driver for JML and JUnit based testing of IntMathOps. |
|
| IntMathOps_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| IntMathOps_JML_TestData
Supply test data for the JML and JUnit based testing of IntMathOps. |
|
| Money
|
|
| MoneyAC
|
|
| MoneyComparable
|
|
| MoneyComparableAC
|
|
| MoneyOps
|
|
| PlusAccount
|
|
| PlusAccount_JML_Test
Automatically-generated test driver for JML and JUnit based testing of PlusAccount. |
|
| PlusAccount_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| PlusAccount_JML_TestData
Supply test data for the JML and JUnit based testing of PlusAccount. |
|
| Point2D
|
|
| Point2D_JML_Test
Automatically-generated test driver for JML and JUnit based testing of Point2D. |
|
| Point2D_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| Point2D_JML_TestData
Supply test data for the JML and JUnit based testing of Point2D. |
|
| USMoney
|
|
| USMoney_JML_Test
Automatically-generated test driver for JML and JUnit based testing of USMoney. |
|
| USMoney_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| USMoney_JML_TestData
Supply test data for the JML and JUnit based testing of USMoney. |
|
|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||