org.jmlspecs.samples.misc
Class SingleSolution

java.lang.Object
  org.jmlspecs.samples.misc.LinearSearch
      org.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

SingleSolution

public SingleSolution(int n)

Initialize this search problem.

Specifications:

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

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;