Package daikon.derive.binary

Class SequenceSubsequence

Object

Derivation

BinaryDerivation

SequenceSubsequence

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

SequenceFloatSubsequence, SequenceScalarSubsequence, SequenceStringSubsequence

public abstract class SequenceSubsequence
extends BinaryDerivation

Derivations of the form A[0..i] or A[i..end], derived from A and i.

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field	Description
boolean	from_start
int	index_shift

Fields inherited from class BinaryDerivation

base1, base2

Fields inherited from class Derivation

debug, dkconfig_disable_derived_variables, missing_array_bounds

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	SequenceSubsequence(VarInfo vi1, VarInfo vi2, boolean from_start, boolean off_by_one)

Method Summary

Modifier and Type	Method	Description
int	complexity()	Adds one to the default complexity if index_shift is not 0.
String	csharp_name(String index)	Returns the name of this variable in CSHARPCONTRACT format.
String	esc_name(String index)	Returns the ESC name.
VarInfo	get_array_var()	Returns the array variable for this slice.
Quantify.Term	get_lower_bound()	Returns the lower bound of the slice.
Quantify.Term	get_upper_bound()	Returns the upper bound of the slice.
String	jml_name(String index)	returns the JML name for the slice
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	seqvar()

Methods inherited from class BinaryDerivation

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

Methods inherited from class Derivation

getVarInfo, inside_csharp_name, inside_esc_name, inside_jml_name, is_prestate_version, isSameFormula, makeVarInfo_common_setup, missingOutOfBounds, shift_str, simplify_name

Methods inherited from class Object

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

Field Detail

index_shift

public final int index_shift

from_start

public final boolean from_start

Constructor Detail

SequenceSubsequence

protected SequenceSubsequence(VarInfo vi1,
                              VarInfo vi2,
                              boolean from_start,
                              boolean off_by_one)

Parameters:

from_start - true means the range goes 0..n; false means the range goes n..end. (n might be fudged through off_by_one.)

off_by_one - true means we should exclude the scalar from the range; false means we should include it

Method Detail

seqvar

public VarInfo seqvar(@GuardSatisfied SequenceSubsequence this)

sclvar

public VarInfo sclvar(@GuardSatisfied SequenceSubsequence this)

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

get_lower_bound

public Quantify.Term get_lower_bound()

Returns the lower bound of the slice.

Overrides:

get_lower_bound in class Derivation

get_upper_bound

public Quantify.Term get_upper_bound()

Returns the upper bound of the slice.

Overrides:

get_upper_bound in class Derivation

get_array_var

public VarInfo get_array_var()

Returns the array variable for this slice.

Overrides:

get_array_var in class Derivation

csharp_name

@SideEffectFree
public String csharp_name(String index)

Description copied from class: Derivation

Returns the name of this variable in CSHARPCONTRACT format. If an index is specified, it is used as an array index. It is an error to specify an index on a non-array variable.

Overrides:

csharp_name in class 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 for the slice

Overrides:

jml_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