Package daikon.derive.binary

Class SequencesPredicate

Object

Derivation

BinaryDerivation

SequencesPredicate

All Implemented Interfaces:

Serializable, Cloneable

public final class SequencesPredicate
extends BinaryDerivation

Derived variable representing the selecting of elements of one sequence based on the values of another sequence. We only predicate if we know that both sequences came from the same original data structure. Derived type is the same as that of the first sequence.

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field	Description
static Logger	debug	Debug tracer.
static boolean	dkconfig_boolOnly	Boolean.
static boolean	dkconfig_enabled	Boolean.
static boolean	dkconfig_fieldOnly	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 subset of val1 such that the corresponding element in var2 equals this.choose.
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 SequencesPredicate derived variables should be generated.

dkconfig_fieldOnly

public static boolean dkconfig_fieldOnly

Boolean. True if Daikon should only generate derivations on fields of the same data structure.

dkconfig_boolOnly

public static boolean dkconfig_boolOnly

Boolean. True if Daikon should only generate derivations on boolean predicates.

Method Detail

var1

public VarInfo var1(@GuardSatisfied SequencesPredicate this)

Overrides:

var1 in class BinaryDerivation

var2

public VarInfo var2(@GuardSatisfied SequencesPredicate this)

Overrides:

var2 in class BinaryDerivation

computeValueAndModifiedImpl

public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt)

Returns a subset of val1 such that the corresponding element in var2 equals this.choose. It is assumed that val1 and val2 originated from the same, larger data structure.

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 SequencesPredicate 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