SequenceStringSubsequence

Object
- Derivation
- - BinaryDerivation
  - - SequenceSubsequence
    - - SequenceStringSubsequence

All Implemented Interfaces:: Serializable, Cloneable

public final class SequenceStringSubsequence
extends SequenceSubsequence

See Also:: Serialized Form

Field Summary

Fields
Modifier and Type Field Description

static boolean dkconfig_enabled
Boolean.
- Fields inherited from class SequenceSubsequence
  from_start, index_shift
- Fields inherited from class BinaryDerivation
  base1, base2
- Fields inherited from class Derivation
  debug, dkconfig_disable_derived_variables, missing_array_bounds

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`ValueAndModified`	`computeValueAndModifiedImpl(ValueTuple full_vt)`	Actual implementation once mods are handled.
`boolean`	`isSameFormula(Derivation other)`	Returns true iff other and this represent the same derivation (modulo the variable they are applied to).
`String`	`toString()`

Methods inherited from class SequenceSubsequence
complexity, csharp_name, esc_name, get_array_var, get_lower_bound, get_upper_bound, jml_name, makeVarInfo, sclvar, seqvar

Methods inherited from class BinaryDerivation
canBeMissing, clone, computeValueAndModified, 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, makeVarInfo_common_setup, missingOutOfBounds, shift_str, simplify_name

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 SequenceStringSubsequence derived variables should be generated.
- Method Detail
  - toString
```
@SideEffectFree
public String toString(@GuardSatisfied SequenceStringSubsequence 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
  - 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