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
All Methods Instance Methods Concrete Methods 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 name of this variable in ESC format.VarInfo
get_array_var()
Returns the array variable that underlies this slice.Quantify.Term
get_lower_bound()
Returns the lower bound of a slice.Quantify.Term
get_upper_bound()
Returns the lower bound of a slice.String
jml_name(String index)
Returns the name of this variable in JML format.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
-
-
-
-
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
-
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 classDerivation
-
get_lower_bound
public Quantify.Term get_lower_bound()
Description copied from class:Derivation
Returns the lower bound of a slice. Throws an error if this is not a slice. Slices should override.- Overrides:
get_lower_bound
in classDerivation
-
get_upper_bound
public Quantify.Term get_upper_bound()
Description copied from class:Derivation
Returns the lower bound of a slice. Throws an error if this is not a slice. Slices should override.- Overrides:
get_upper_bound
in classDerivation
-
get_array_var
public VarInfo get_array_var()
Description copied from class:Derivation
Returns the array variable that underlies this slice. Throws an error if this is not a slice. Slices should override.- Overrides:
get_array_var
in classDerivation
-
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 classDerivation
-
esc_name
@SideEffectFree public String esc_name(String index)
Description copied from class:Derivation
Returns the name of this variable in ESC 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:
esc_name
in classDerivation
-
jml_name
public String jml_name(String index)
Description copied from class:Derivation
Returns the name of this variable in JML 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:
jml_name
in classDerivation
-
complexity
public int complexity()
Adds one to the default complexity if index_shift is not 0.- Overrides:
complexity
in classDerivation
-
-