org.jmlspecs.jmlunit.strategies
Class ImmutableObjectExtensibleStrategyDecorator

java.lang.Object
  org.jmlspecs.jmlunit.strategies.AbstractExtensibleStrategyDecorator
      org.jmlspecs.jmlunit.strategies.ImmutableObjectExtensibleStrategyDecorator

All Implemented Interfaces:

StrategyType

public class ImmutableObjectExtensibleStrategyDecorator

extends AbstractExtensibleStrategyDecorator

A decorator for immutable object strategies that allows for easy extension with immutable test data.

This type provides an extension mechanism that is easier to use than a composite. To extend the test data, make a subclass that overrides the addData() method; this method provides the additional data for testing.

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

addedData, defaultData

 

Constructor Summary

ImmutableObjectExtensibleStrategyDecorator(StrategyType strat)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
protected  StrategyType	addedDataStrategy(final Object[] added)

 

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

addData, iterator

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

ImmutableObjectExtensibleStrategyDecorator

public ImmutableObjectExtensibleStrategyDecorator(StrategyType strat)

Specifications:

public normal_behavior
requires strat != null;
assignable defaultData, addedData, objectState;
ensures this.defaultData == strat;

addedDataStrategy

protected StrategyType addedDataStrategy(final Object[] added)

Specifications inherited from overridden method addedDataStrategy(Object[] added) in class AbstractExtensibleStrategyDecorator:

protected normal_behavior
requires added != null;
assignable addedData, objectState;
ensures \result != null;