org.jmlspecs.jmlunit.strategies
Class CloneableObjectAbstractExtensibleStrategyDecorator

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

All Implemented Interfaces:

StrategyType

Direct Known Subclasses:

JMLTypeStrategy

public abstract class CloneableObjectAbstractExtensibleStrategyDecorator

extends AbstractExtensibleStrategyDecorator

A decorator for cloneable object strategies that allows for easy extension with cloneable 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

CloneableObjectAbstractExtensibleStrategyDecorator(StrategyType strat)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
protected  StrategyType	addedDataStrategy(final Object[] added)
abstract  Object	cloneElement(Object elem)           Return a clone of the argument.

 

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

CloneableObjectAbstractExtensibleStrategyDecorator

public CloneableObjectAbstractExtensibleStrategyDecorator(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;

cloneElement

public abstract Object cloneElement(Object elem)

Return a clone of the argument.

Specifications: pure

protected normal_behavior
requires elem != null;
assignable \nothing;
ensures \result != null&&\result .equals(elem);