Class SingleSolution

  extended byorg.jmlspecs.samples.misc.LinearSearch
      extended byorg.jmlspecs.samples.misc.SingleSolution
Direct Known Subclasses:
EqualsN, LessThanN

public abstract class SingleSolution
extends LinearSearch

A class of search problems for which there is one solution.

Class Specifications

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
Ghost Field Summary
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
Field Summary
[spec_public] protected  int n
          The number sought.
Constructor Summary
SingleSolution(int n)
          Initialize this search problem.
Model Method Summary
Model methods inherited from class java.lang.Object
Method Summary
protected abstract  String className()
          A hook method for defining toString.
 int limit()
 String toString()
Methods inherited from class org.jmlspecs.samples.misc.LinearSearch
f, find
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail


protected int n
The number sought.

Specifications: spec_public
Constructor Detail


public SingleSolution(int n)
Initialize this search problem.

assignable this.n;
ensures this.n == n;
Method Detail


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

Specifications: pure
Specifications inherited from overridden method in class LinearSearch:
ensures 0 <= \result ;
ensures ( \exists int j; 0 <= j&&j <= \result ; this.f(j));


public String toString()
toString in class Object
ensures \result != null;
Specifications inherited from overridden method in class Object:
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
public code model_program { ... }
assignable objectState;
ensures \result != null;


protected abstract String className()
A hook method for defining toString.

Specifications: pure
ensures \result != null;


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.