|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use org.jmlspecs.samples.misc | |
| org.jmlspecs.samples.misc | This package contains miscellaneous samples of JML specifications. |
| Classes in org.jmlspecs.samples.misc used by org.jmlspecs.samples.misc | |
| Counter
A simple Counter. |
|
| Counter_JML_Test
Automatically-generated test driver for JML and JUnit based testing of Counter. |
|
| Counter_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| Counter_JML_TestData
Supply test data for the JML and JUnit based testing of Counter. |
|
| LinearSearch
A linear search component, intended to demonstrate verification in JML specifications. |
|
| LinearSearch_JML_Test
Automatically-generated test driver for JML and JUnit based testing of LinearSearch. |
|
| LinearSearch_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| LinearSearch_JML_TestData
Supply test data for the JML and JUnit based testing of LinearSearch. |
|
| Meter
A behavioral subtype of Counter. |
|
| Meter_JML_Test
Automatically-generated test driver for JML and JUnit based testing of Meter. |
|
| Meter_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| Meter_JML_TestData
Supply test data for the JML and JUnit based testing of Meter. |
|
| Proof
A class that demonstrates Floyd-Hoare-style proofs using JML notation. |
|
| Proof_JML_Test
Automatically-generated test driver for JML and JUnit based testing of Proof. |
|
| Proof_JML_Test.OneTest
A JUnit test object that can run a single test method. |
|
| Proof_JML_TestData
Supply test data for the JML and JUnit based testing of Proof. |
|
| SingleSolution
A class of search problems for which there is one solution. |
|
|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||