Package daikon.derive.binary

Class SequencesJoinFloat

Object

Derivation

BinaryDerivation

SequencesJoinFloat

All Implemented Interfaces:

Serializable, Cloneable

public final class SequencesJoinFloat
extends BinaryDerivation

Derived variable representing the "join" of two sequences. That is, if the two sequences came from the same original data structure (like an array of multi-field objects) then we join the two sequences and generate a hashcode of the join value. This allows us to detect uniqueness and equality style invariants across the data structure rather than just one slice of it. Works for number and string arrays.

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field	Description
static Logger	debug	Debug tracer.
static boolean	dkconfig_enabled	Boolean.

Fields inherited from class BinaryDerivation

base1, base2

Fields inherited from class Derivation

dkconfig_disable_derived_variables, missing_array_bounds

Method Summary

Modifier and Type	Method	Description
ValueAndModified	computeValueAndModifiedImpl(ValueTuple full_vt)	Returns a new sequence of hashcodes that is the join of the hashcodes of the component sequences.
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).
protected VarInfo	makeVarInfo()	Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().
String	toString()
VarInfo	var1()
VarInfo	var2()

Methods inherited from class BinaryDerivation

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

Methods inherited from class Derivation

complexity, csharp_name, get_array_var, get_lower_bound, get_upper_bound, getVarInfo, inside_csharp_name, inside_esc_name, inside_jml_name, is_prestate_version, jml_name, makeVarInfo_common_setup, missingOutOfBounds, shift_str, simplify_name

Methods inherited from class Object

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

Field Detail

debug

public static final Logger debug

Debug tracer.

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff SequencesJoin derived variables should be generated.

Method Detail

var1

public VarInfo var1(@GuardSatisfied SequencesJoinFloat this)

Overrides:

var1 in class BinaryDerivation

var2

public VarInfo var2(@GuardSatisfied SequencesJoinFloat this)

Overrides:

var2 in class BinaryDerivation

computeValueAndModifiedImpl

public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt)

Returns a new sequence of hashcodes that is the join of the hashcodes of the component sequences. This is modified whenever either component sequence is modified.

Specified by:

computeValueAndModifiedImpl in class BinaryDerivation

Parameters:

full_vt - the value tuple of a program point to compute the derived value from

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

toString

@SideEffectFree
public String toString(@GuardSatisfied SequencesJoinFloat this)

Overrides:

toString in class Object

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