Object
- Invariant
- - UnaryInvariant
  - - SingleSequence
    - - SingleScalarSequence
      - SeqIndexIntLessEqual

All Implemented Interfaces:

Serializable, Cloneable
```
public class SeqIndexIntLessEqual
extends SingleScalarSequence
```
Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as x[i] <= i.

See Also:

Serialized Form

Nested Class Summary
- Nested classes/interfaces inherited from class Invariant
  Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match

Field Summary

Fields
Modifier and Type Field Description

static Logger debug
Debug tracer.

static boolean dkconfig_enabled
Boolean.
- Fields inherited from class SingleSequence
  dkconfig_SeqIndexDisableAll
- Fields inherited from class Invariant
  checkedMergeOverridden, CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debugFlow, debugGuarding, debugIsObvious, debugIsWorthPrinting, debugPrint, debugPrintEquality, dkconfig_confidence_limit, dkconfig_fuzzy_ratio, dkconfig_simplify_define_predicates, falsified, invariantEnabledDefault, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Constructor Summary

Constructors
Modifier Constructor Description

protected SeqIndexIntLessEqual(PptSlice slice)

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`InvariantStatus`	`add_modified(long @Interned [] a, int count)`	Similar to `SingleScalarSequence.check_modified(long[], int)` except that it can change the state of the invariant if necessary.
`InvariantStatus`	`check_modified(long @Interned [] a, int count)`	Presents a sample to the invariant.
`protected double`	`computeConfidence()`	This method computes the confidence that this invariant occurred by chance.
`boolean`	`enabled()`	Returns whether or not this class of invariants is currently enabled.
`static @Nullable SeqIndexIntLessEqual`	`find(PptSlice ppt)`
`String`	`format_csharp_contract()`
`String`	`format_daikon()`
`String`	`format_esc()`
`String`	`format_java_family(OutputFormat format)`
`String`	`format_simplify()`
`String`	`format_using(OutputFormat format)`	Return a printed representation of this invariant, in the given format.
`NISuppressionSet`	`get_ni_suppressions()`	returns the ni-suppressions for SeqIndexIntLessEqual
`static SeqIndexIntLessEqual`	`get_proto()`	Returns the prototype invariant for SeqIndexIntLessEqual
`String`	`getComparator()`
`SeqIndexIntLessEqual`	`instantiate_dyn(PptSlice slice)`	Instantiates (creates) an invariant of the same class on the specified slice.
`boolean`	`instantiate_ok(VarInfo[] vis)`	Returns true if it makes sense to instantiate this invariant over the specified variables.
`boolean`	`isExclusiveFormula(Invariant other)`	Returns true iff the two invariants represent mutually exclusive mathematical formulas -- that is, if one of them is true, then the other must be false.
`@Nullable DiscardInfo`	`isObviousDynamically(VarInfo[] vis)`	Checks to see if this is obvious over the specified variables Implements the following checks:
`boolean`	`isSameFormula(Invariant other)`	Returns true iff the two invariants represent the same mathematical formula.
`protected Invariant`	`resurrect_done_swapped()`

Methods inherited from class SingleScalarSequence
add, add_unmodified, check, check_unmodified, valid_types, valid_types_static, var

Methods inherited from class UnaryInvariant
resurrect_done

Methods inherited from class Invariant
add_sample, asInvClass, checkRep, clear_falsified, clone, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, merge, mergeFormulasOk, permute, prob_and, prob_and, prob_is_ge, prob_or, repCheck, repr, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames

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 SeqIndexIntLessEqual invariants should be considered.
- Constructor Detail
  - SeqIndexIntLessEqual
```
protected SeqIndexIntLessEqual(PptSlice slice)
```
- Method Detail
  - get_proto
```
public static SeqIndexIntLessEqual get_proto()
```
    Returns the prototype invariant for SeqIndexIntLessEqual
  - enabled
```
public boolean enabled()
```
    Description copied from class: Invariant
    
    Returns whether or not this class of invariants is currently enabled.
    Its implementation is almost always return dkconfig_enabled;.
    
    Specified by:
    
    enabled in class Invariant
  - instantiate_ok
```
public boolean instantiate_ok(VarInfo[] vis)
```
    Description copied from class: Invariant
    
    Returns true if it makes sense to instantiate this invariant over the specified variables. Checks details beyond what is provided by Invariant.valid_types(daikon.VarInfo[]). This should never be called without calling valid_types() first (implementations should be able to presume that valid_types() returns true).
    This method does not have to be overridden; the default implementation in Invariant returns true.
    
    Overrides:
    
    instantiate_ok in class Invariant
    
    See Also:
    
    Invariant.valid_types(VarInfo[])
  - instantiate_dyn
```
public SeqIndexIntLessEqual instantiate_dyn( SeqIndexIntLessEqual this,
                                            PptSlice slice)
```
    Description copied from class: Invariant
    
    Instantiates (creates) an invariant of the same class on the specified slice. Must be overridden in each class. Must be used rather than Invariant.clone() so that checks in Invariant.instantiate(daikon.PptSlice) for reasonable invariants are done.
    The implementation of this method is almost always return new <em>InvName</em>(slice);
    
    Specified by:
    
    instantiate_dyn in class Invariant
    
    Returns:
    
    the new invariant
  - get_ni_suppressions
```
@Pure
public NISuppressionSet get_ni_suppressions()
```
    returns the ni-suppressions for SeqIndexIntLessEqual
    
    Overrides:
    
    get_ni_suppressions in class Invariant
    
    Returns:
    
    the set of non-instantiating suppressions for this invariant
  - resurrect_done_swapped
```
protected Invariant resurrect_done_swapped()
```
  - getComparator
```
public String getComparator()
```
  - format_using
```
@SideEffectFree
public String format_using(@GuardSatisfied SeqIndexIntLessEqual this,
                           OutputFormat format)
```
    Description copied from class: Invariant
    
    Return a printed representation of this invariant, in the given format.
    
    Specified by:
    
    format_using in class Invariant
  - format_daikon
```
public String format_daikon(@GuardSatisfied SeqIndexIntLessEqual this)
```
  - format_esc
```
public String format_esc(@GuardSatisfied SeqIndexIntLessEqual this)
```
  - format_csharp_contract
```
public String format_csharp_contract(@GuardSatisfied SeqIndexIntLessEqual this)
```
  - format_java_family
```
public String format_java_family(@GuardSatisfied SeqIndexIntLessEqual this,
                                 OutputFormat format)
```
  - format_simplify
```
public String format_simplify(@GuardSatisfied SeqIndexIntLessEqual this)
```
  - check_modified
```
public InvariantStatus check_modified(long @Interned [] a,
                                      int count)
```
    Description copied from class: SingleScalarSequence
    
    Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.
    
    Specified by:
    
    check_modified in class SingleScalarSequence
    
    count - how many identical samples were observed in a row. For example, three calls to check_modified with a count parameter of 1 is equivalent to one call to check_modified with a count parameter of 3.
    
    Returns:
    
    whether or not the sample is consistent with the invariant
  - add_modified
```
public InvariantStatus add_modified(long @Interned [] a,
                                    int count)
```
    Description copied from class: SingleScalarSequence
    
    Similar to SingleScalarSequence.check_modified(long[], int) except that it can change the state of the invariant if necessary. If the invariant doesn't have any state, then the implementation should simply call SingleScalarSequence.check_modified(long[], int). This method need not check for falsification; that is done by the caller.
    
    Specified by:
    
    add_modified in class SingleScalarSequence
  - computeConfidence
```
protected double computeConfidence()
```
    Description copied from class: Invariant
    
    This method computes the confidence that this invariant occurred by chance. Clients should call Invariant.getConfidence() instead.
    This method need not check the value of field "falsified", as the caller does that.
    
    Specified by:
    
    computeConfidence in class Invariant
    
    Returns:
    
    confidence of this invariant
    
    See Also:
    
    Invariant.getConfidence()
  - isSameFormula
```
@Pure
public boolean isSameFormula(Invariant other)
```
    Description copied from class: Invariant
    
    Returns true iff the two invariants represent the same mathematical formula. Does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities. As a rule of thumb, if two invariants format the same, this method returns true. Furthermore, in many cases, if an invariant does not involve computed constants (as "x>c" and "y=ax+b" do for constants a, b, and c), then this method vacuously returns true.
    
    Specified by:
    
    isSameFormula in class Invariant
    
    Parameters:
    
    other - the invariant to compare to this one
    
    Returns:
    
    true iff the two invariants represent the same mathematical formula. Does not consider
  - isExclusiveFormula
```
@Pure
public boolean isExclusiveFormula(Invariant other)
```
    Description copied from class: Invariant
    
    Returns true iff the two invariants represent mutually exclusive mathematical formulas -- that is, if one of them is true, then the other must be false. This method does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities.
    
    Overrides:
    
    isExclusiveFormula in class Invariant
    
    Parameters:
    
    other - the other invariant to compare to this one
    
    Returns:
    
    true iff the two invariants represent mutually exclusive mathematical formulas
  - find
```
public static @Nullable SeqIndexIntLessEqual find(PptSlice ppt)
```
  - isObviousDynamically
```
@Pure
public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis)
```
    Checks to see if this is obvious over the specified variables Implements the following checks:
    (A[] subsequence B[]) ^ (B[i] op i) ⇒ A[i] op i
    JHP: Its not obvious (to me) that this is true except when the subsequence starts at index 0. If B[] = {0, 1, 2, 3, 4} and A[] = {2, 3, 4}, A[] is a subsequence of B[] and B[i] == i, but A[i] = i is not true.
    Overrides:
    
    isObviousDynamically in class Invariant

Modifier and Type	Field	Description
`static Logger`	`debug`	Debug tracer.
`static boolean`	`dkconfig_enabled`	Boolean.

Class SeqIndexIntLessEqual

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

Field Summary

Fields inherited from class SingleSequence

Fields inherited from class Invariant

Constructor Summary

Method Summary

Methods inherited from class SingleScalarSequence

Methods inherited from class UnaryInvariant

Methods inherited from class Invariant

Methods inherited from class Object

Field Detail

debug

dkconfig_enabled

Constructor Detail

SeqIndexIntLessEqual

Method Detail

get_proto

enabled

instantiate_ok

instantiate_dyn

get_ni_suppressions

resurrect_done_swapped

getComparator

format_using

format_daikon

format_esc

format_csharp_contract

format_java_family

format_simplify

check_modified

add_modified

computeConfidence

isSameFormula

isExclusiveFormula

find

isObviousDynamically