Package org.jmlspecs.samples.misc

This package contains miscellaneous samples of JML specifications.

See:
Description

Interface Summary

Counter

A simple Counter.

Class Summary

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_Test.TestInc	Test for the inc method.
Counter_JML_Test.TestValue	Test for the value method.
Counter_JML_TestData	Supply test data for the JML and JUnit based testing of Counter.
EqualsN	A search problem which is to find the number n.
LessThanN	A search problem which is to find the first number strictly less than n (and greater than 0).
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_Test.TestF	Test for the f method.
LinearSearch_JML_Test.TestFind	Test for the find method.
LinearSearch_JML_Test.TestLimit	Test for the limit 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_Test.TestInc	Test for the inc method.
Meter_JML_Test.TestMeter	Test for the Meter contructor.
Meter_JML_Test.TestValue	Test for the value 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_Test.TestFind	Test for the find method.
Proof_JML_Test.TestFind_min	Test for the find_min method.
Proof_JML_Test.TestGetRes	Test for the getRes 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.
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.misc Description

This package contains miscellaneous samples of JML specifications. Many of these are related to verification issues, and some are illustrating points about behavioral subtyping.