DoubleBigStrategy (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jmlunit.strategies
Class DoubleBigStrategy

java.lang.Object
  org.jmlspecs.jmlunit.strategies.DoubleAbstractStrategy
      org.jmlspecs.jmlunit.strategies.DoubleExtensibleStrategyDecorator
          org.jmlspecs.jmlunit.strategies.DoubleBigStrategy

All Implemented Interfaces:: DoubleStrategyType, StrategyType

Direct Known Subclasses:: DoubleAbstractFilteringIteratorDecorator_JML_TestData.DoubleAbstractFilteringIteratorDecorator_JML_TestData$1, Point2D_JML_TestData.Point2D_JML_TestData$2, SqrtExample_JML_TestData.SqrtExample_JML_TestData$1, USMoney_JML_TestData.USMoney_JML_TestData$1

public class DoubleBigStrategy
extends DoubleExtensibleStrategyDecorator

Slightly more extensive test data of type double.

Subclasses of this strategy can provide additional test data by overriding the method addData().

Author:: Gary T. Leavens
See Also:: DoubleStrategy

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.jmlunit.strategies.DoubleExtensibleStrategyDecorator

addedData, defaultData

Constructor Summary

DoubleBigStrategy()
Initialize this strategy.

Model Method Summary

Model methods inherited from class java.lang.Object

hashValue

Method Summary

protected double[] defaultData()

Methods inherited from class org.jmlspecs.jmlunit.strategies.DoubleExtensibleStrategyDecorator

addData, doubleIterator

Methods inherited from class org.jmlspecs.jmlunit.strategies.DoubleAbstractStrategy

iterator

Methods inherited from class java.lang.Object

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

Constructor Detail

DoubleBigStrategy

public DoubleBigStrategy()

Initialize this strategy.

Specifications:: public normal_behavior
assignable defaultData, addedData;

Method Detail

defaultData

protected double[] defaultData()