Package daikon.derive.binary

Class SequenceScalarSubscript

Object

Derivation

BinaryDerivation

SequenceScalarSubscript

All Implemented Interfaces:

Serializable, Cloneable

public final class SequenceScalarSubscript
extends BinaryDerivation

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field	Description
static Logger	debug	General debug tracer.
static boolean	dkconfig_enabled	Boolean.
int	index_shift

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
int	complexity()	Adds one to the default complexity if index_shift is not 0.
ValueAndModified	computeValueAndModifiedImpl(ValueTuple full_vt)	Actual implementation once mods are handled.
String	csharp_name(String index)	Returns the CSHARPCONTRACT name for sequence subscript.
String	esc_name(String index)	Returns the ESC name for sequence subscript.
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 for sequence subscript.
protected VarInfo	makeVarInfo()	Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().
VarInfo	sclvar()
VarInfo	seq_enclosing_var()
VarInfo	seqvar()
String	simplify_name()	Return the simplify name for sequence subscript.
String	toString()

Methods inherited from class BinaryDerivation

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

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, wait, wait, wait

Field Detail

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff SequenceScalarSubscript derived variables should be generated.

debug

public static final Logger debug

General debug tracer.

index_shift

public final int index_shift

Method Detail

seqvar

public VarInfo seqvar(@GuardSatisfied SequenceScalarSubscript this)

sclvar

public VarInfo sclvar(@GuardSatisfied SequenceScalarSubscript this)

seq_enclosing_var

public VarInfo seq_enclosing_var()

toString

@SideEffectFree
public String toString(@GuardSatisfied SequenceScalarSubscript this)

Overrides:

toString in class Object

computeValueAndModifiedImpl

public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt)

Description copied from class: BinaryDerivation

Actual implementation once mods are handled.

Specified by:

computeValueAndModifiedImpl in class BinaryDerivation

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 for sequence subscript.

Overrides:

esc_name in class Derivation

jml_name

public String jml_name(String index)

Returns the JML name for sequence subscript.

Overrides:

jml_name in class Derivation

csharp_name

@SideEffectFree
public String csharp_name(String index)

Returns the CSHARPCONTRACT name for sequence subscript.

Overrides:

csharp_name in class Derivation

simplify_name

@SideEffectFree
public String simplify_name()

Return the simplify name for sequence subscript.

Overrides:

simplify_name in class Derivation

complexity

public int complexity()

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

Overrides:

complexity in class Derivation