JML

org.jmlspecs.samples.misc
Class SingleSolution

java.lang.Object
  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
hashValue
 
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

n

protected int n
The number sought.

Specifications: spec_public
Constructor Detail

SingleSolution

public SingleSolution(int n)
Initialize this search problem.

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

limit

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:
       pure
ensures 0 <= \result ;
ensures ( \exists int j; 0 <= j&&j <= \result ; this.f(j));

toString

public String toString()
Overrides:
toString in class Object
Specifications:
     also
ensures \result != null;
Specifications inherited from overridden method in class Object:
       non_null
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
     also
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 *);
     also
public code model_program { ... }
    implies_that
assignable objectState;
ensures \result != null;

className

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

Specifications: pure
ensures \result != null;

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.