JML

org.jmlspecs.samples.misc
Class LinearSearch

java.lang.Object
  extended byorg.jmlspecs.samples.misc.LinearSearch
Direct Known Subclasses:
SingleSolution

public abstract class LinearSearch
extends Object

A linear search component, intended to demonstrate verification in JML specifications. This class has two abstract methods that describe the search, which need to be filled in to instantiate it. The formulation of the search and the verification is based on Edward Cohen's book Programming in the 1990s (Springer-Verlag, 1990).

Author:
Gary T. Leavens

Constructor Summary
LinearSearch()
           
 
Method Summary
abstract  boolean f(int j)
          The function that describes what is being sought.
 int find()
          Find a solution to the searching problem.
abstract  int limit()
          The last integer in the search space, this describes the domain of f, which goes from 0 to the result.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

LinearSearch

public LinearSearch()
Method Detail

f

public abstract boolean f(int j)
The function that describes what is being sought.


limit

public abstract int limit()
The last integer in the search space, this describes the domain of f, which goes from 0 to the result.


find

public int find()
Find a solution to the searching problem.


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.