org.jmlspecs.samples.misc
Class EqualsN

java.lang.Object
  org.jmlspecs.samples.misc.LinearSearch
      org.jmlspecs.samples.misc.SingleSolution
          org.jmlspecs.samples.misc.EqualsN

public class EqualsN

extends SingleSolution

A search problem which is to find the number n.

Author:

Gary T. Leavens

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

 

Fields inherited from class org.jmlspecs.samples.misc.SingleSolution

n

 

Constructor Summary

EqualsN(int n)           Initialize this search problem.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
protected  String	className()
boolean	f(int j)

 

Methods inherited from class org.jmlspecs.samples.misc.SingleSolution

limit, toString

 

Methods inherited from class org.jmlspecs.samples.misc.LinearSearch

find

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Constructor Detail

EqualsN

public EqualsN(int n)

Initialize this search problem.

Specifications:

assignable this.n;
ensures this.n == n;

f

public boolean f(int j)

Description copied from class: LinearSearch

The function that describes what is being sought.

Specifications: pure

     also

requires j >= 0;
ensures \result <==> j == this.n;

Specifications inherited from overridden method f(int j) in class LinearSearch:
       pure

requires j >= 0;

className

protected String className()

Description copied from class: SingleSolution

A hook method for defining toString.

Specifications: (inherited)pure

Specifications inherited from overridden method in class SingleSolution:
       pure

ensures \result != null;