Overview   Package  Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV PACKAGE   NEXT PACKAGE FRAMES    NO FRAMES    

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_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_TestData Supply test data for the JML and JUnit based testing of LinearSearch.
Meter A behavioral subtype of Counter.
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_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.
 

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.

Overview   Package  Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV PACKAGE   NEXT PACKAGE FRAMES    NO FRAMES    
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.