Package daikon.derive.unary

Class SequenceLength

Object

Derivation

UnaryDerivation

SequenceLength

All Implemented Interfaces:

Serializable, Cloneable

public final class SequenceLength
extends UnaryDerivation

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field	Description
static boolean	dkconfig_enabled	Boolean.
int	shift

Fields inherited from class UnaryDerivation

base

Fields inherited from class Derivation

debug, dkconfig_disable_derived_variables, missing_array_bounds

Constructor Summary

Constructors

Constructor	Description
SequenceLength(VarInfo vi, int shift)

Method Summary

Modifier and Type	Method	Description
static boolean	applicable(VarInfo vi)
int	complexity()	Adds one to the default complexity if shift is not 0.
ValueAndModified	computeValueAndModifiedImpl(ValueTuple vt)	Actual implementation once mods are handled.
String	csharp_name(String index)	Returns the CSharpContract name.
String	esc_name(String index)	Returns the ESC name.
boolean	isSameFormula(Derivation other)	Returns true iff other and this represent the same derivation (modulo the variable they are applied to).
String	jml_name(String index)	Returns the JML name.
protected VarInfo	makeVarInfo()	Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().
String	simplify_name()	Returns the Simplify name.

Methods inherited from class UnaryDerivation

base, canBeMissing, clone, computeValueAndModified, derivedDepth, getBase, getBases, isDerivedFromNonCanonical, isParam, switchVars

Methods inherited from class Derivation

get_array_var, get_lower_bound, get_upper_bound, getVarInfo, inside_csharp_name, inside_esc_name, inside_jml_name, is_prestate_version, makeVarInfo_common_setup, missingOutOfBounds, shift_str

Methods inherited from class Object

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

Field Detail

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff SequenceLength derived variables should be generated.

shift

public final int shift

Constructor Detail

SequenceLength

public SequenceLength(VarInfo vi,
                      int shift)

Method Detail

applicable

public static boolean applicable(VarInfo vi)

computeValueAndModifiedImpl

public ValueAndModified computeValueAndModifiedImpl(ValueTuple vt)

Description copied from class: UnaryDerivation

Actual implementation once mods are handled.

Specified by:

computeValueAndModifiedImpl in class UnaryDerivation

makeVarInfo

protected VarInfo makeVarInfo()

Description copied from class: Derivation

Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().

Specified by:

makeVarInfo in class Derivation

isSameFormula

@Pure
public boolean isSameFormula(Derivation other)

Description copied from class: Derivation

Returns true iff other and this represent the same derivation (modulo the variable they are applied to). Default implentation will just checks run-time type, but subclasses with state (e.g. SequenceInitial index) should match that, too.

Specified by:

isSameFormula in class Derivation

Parameters:

other - the Derivation to compare to

Returns:

true iff other and this represent the same derivation

esc_name

@SideEffectFree
public String esc_name(String index)

Returns the ESC name.

Overrides:

esc_name in class Derivation

jml_name

public String jml_name(String index)

Returns the JML name.

Overrides:

jml_name in class Derivation

simplify_name

@SideEffectFree
public String simplify_name()

Returns the Simplify name.

Overrides:

simplify_name in class Derivation

csharp_name

@SideEffectFree
public String csharp_name(String index)

Returns the CSharpContract name.

Overrides:

csharp_name in class Derivation

complexity

public int complexity()

Adds one to the default complexity if shift is not 0.

Overrides:

complexity in class Derivation