JML

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.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.