Object
- Invariant
- - BinaryInvariant
  - - TwoSequence
    - - PairwiseIntLessEqual

All Implemented Interfaces:

Serializable, Cloneable
```
public class PairwiseIntLessEqual
extends TwoSequence
```
Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each (x[i], y[i]) pair. Thus, x[0] is compared to y[0], x[1] to y[1], and so forth. Prints as x[] <= y[].

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 TwoSequence
  swap
- Fields inherited from class Invariant
  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`	`PairwiseIntLessEqual()`
`protected`	`PairwiseIntLessEqual(PairwiseIntGreaterEqual swapped_pic)`
`protected`	`PairwiseIntLessEqual(PptSlice ppt)`

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`InvariantStatus`	`add_modified(long @Interned [] a1, long @Interned [] a2, int count)`	Default implementation simply calls check.
`InvariantStatus`	`check_modified(long @Interned [] a1, long @Interned [] a2, 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 invariant is enabled.
`static @Nullable PairwiseIntLessEqual`	`find(PptSlice ppt)`
`String`	`format_csharp()`
`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.
`@Nullable NISuppressionSet`	`get_ni_suppressions()`	Returns a list of non-instantiating suppressions for this invariant.
`static PairwiseIntLessEqual`	`get_proto()`	Returns the prototype invariant for PairwiseIntLessEqual
`String`	`getComparator()`
`protected PairwiseIntLessEqual`	`instantiate_dyn(PptSlice slice)`	instantiates the invariant on the specified slice
`boolean`	`instantiate_ok(VarInfo[] vis)`	PairwiseIntLessEqual is only valid on integral types.
`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)`	Return non-null if this invariant is necessarily true from a fact that can be determined dynamically (after checking data) -- for the given varInfos rather than the varInfos of this.
`@Nullable DiscardInfo`	`isObviousStatically(VarInfo[] vis)`	Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this.
`boolean`	`isSameFormula(Invariant other)`	Return true if both invariants are the same class and the order of the variables (swap) is the same.
`String`	`repr()`	Returns a representation of the class.
`protected Invariant`	`resurrect_done_swapped()`	Swaps the variables by inverting the state of swap.
`static Class<PairwiseIntGreaterEqual>`	`swap_class()`	Returns the class that corresponds to this class with its variable order swapped.

Methods inherited from class TwoSequence
add, add_unmodified, check, check_unmodified, get_swap, resurrect_done, resurrect_done_unswapped, valid_types, var1, var1, var2, var2

Methods inherited from class BinaryInvariant
add_unordered, check_unordered, find, is_symmetric

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_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_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 PairwiseIntComparison invariants should be considered.
- Constructor Detail
  - PairwiseIntLessEqual
```
protected PairwiseIntLessEqual(PptSlice ppt)
```
  - PairwiseIntLessEqual
```
protected PairwiseIntLessEqual()
```
  - PairwiseIntLessEqual
```
protected PairwiseIntLessEqual(PairwiseIntGreaterEqual swapped_pic)
```
- Method Detail
  - get_proto
```
public static PairwiseIntLessEqual get_proto()
```
    Returns the prototype invariant for PairwiseIntLessEqual
  - enabled
```
public boolean enabled()
```
    Returns whether or not this invariant is enabled.
    
    Specified by:
    
    enabled in class Invariant
  - instantiate_ok
```
public boolean instantiate_ok(VarInfo[] vis)
```
    PairwiseIntLessEqual is only valid on integral types.
    
    Overrides:
    
    instantiate_ok in class Invariant
    
    See Also:
    
    Invariant.valid_types(VarInfo[])
  - instantiate_dyn
```
protected PairwiseIntLessEqual instantiate_dyn( PairwiseIntLessEqual this,
                                               PptSlice slice)
```
    instantiates the invariant on the specified slice
    
    Specified by:
    
    instantiate_dyn in class Invariant
    
    Returns:
    
    the new invariant
  - isObviousStatically
```
@Pure
public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis)
```
    Description copied from class: Invariant
    
    Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this. Conceptually, this means "is this invariant statically obvious if its VarInfos were switched with vis?" Intended to be overridden by subclasses. Should only do static checking.
    Precondition: vis.length == this.ppt.var_infos.length
    
    Overrides:
    
    isObviousStatically in class Invariant
    
    Parameters:
    
    vis - the VarInfos this invariant is obvious over. The position and data type of the variables is the *same* as that of this.ppt.var_infos.
  - isObviousDynamically
```
@Pure
public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis)
```
    Description copied from class: Invariant
    
    Return non-null if this invariant is necessarily true from a fact that can be determined dynamically (after checking data) -- for the given varInfos rather than the varInfos of this. Conceptually, this means, "Is this invariant dynamically obvious if its VarInfos were switched with vis?" Intended to be overriden by subclasses so they can filter invariants after checking; the overriding method should first call "super.isObviousDynamically(vis)". Since this method is dynamic, it should only be called after all processing.
    
    Overrides:
    
    isObviousDynamically in class Invariant
  - resurrect_done_swapped
```
protected Invariant resurrect_done_swapped()
```
    Description copied from class: TwoSequence
    
    Swaps the variables by inverting the state of swap.
    
    Overrides:
    
    resurrect_done_swapped in class TwoSequence
  - swap_class
```
public static Class<PairwiseIntGreaterEqual> swap_class()
```
    Returns the class that corresponds to this class with its variable order swapped.
  - repr
```
public String repr(@GuardSatisfied PairwiseIntLessEqual this)
```
    Description copied from class: TwoSequence
    
    Returns a representation of the class. This includes the classname, variables, and swap state.
    
    Overrides:
    
    repr in class TwoSequence
    
    Returns:
    
    a string representation of this
  - getComparator
```
public String getComparator()
```
  - format_using
```
@SideEffectFree
public String format_using(@GuardSatisfied PairwiseIntLessEqual 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 PairwiseIntLessEqual this)
```
  - format_esc
```
public String format_esc(@GuardSatisfied PairwiseIntLessEqual this)
```
  - format_simplify
```
public String format_simplify(@GuardSatisfied PairwiseIntLessEqual this)
```
  - format_java_family
```
public String format_java_family(@GuardSatisfied PairwiseIntLessEqual this,
                                 OutputFormat format)
```
  - format_csharp
```
public String format_csharp(@GuardSatisfied PairwiseIntLessEqual this)
```
  - check_modified
```
public InvariantStatus check_modified(long @Interned [] a1,
                                      long @Interned [] a2,
                                      int count)
```
    Description copied from class: TwoSequence
    
    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 TwoSequence
    
    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 [] a1,
                                    long @Interned [] a2,
                                    int count)
```
    Description copied from class: TwoSequence
    
    Default implementation simply calls check. Subclasses can override.
    
    Overrides:
    
    add_modified in class TwoSequence
  - 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.
    
    Overrides:
    
    computeConfidence in class TwoSequence
    
    Returns:
    
    confidence of this invariant
    
    See Also:
    
    Invariant.getConfidence()
  - isSameFormula
```
@Pure
public boolean isSameFormula(Invariant other)
```
    Description copied from class: TwoSequence
    
    Return true if both invariants are the same class and the order of the variables (swap) is the same.
    
    Overrides:
    
    isSameFormula in class TwoSequence
    
    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 PairwiseIntLessEqual find(PptSlice ppt)
```
  - get_ni_suppressions
```
@Pure
public @Nullable NISuppressionSet get_ni_suppressions()
```
    Returns a list of non-instantiating suppressions for this invariant.
    
    Overrides:
    
    get_ni_suppressions in class Invariant
    
    Returns:
    
    the set of non-instantiating suppressions for this invariant

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

Class PairwiseIntLessEqual

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

Field Summary

Fields inherited from class TwoSequence

Fields inherited from class Invariant

Constructor Summary

Method Summary

Methods inherited from class TwoSequence

Methods inherited from class BinaryInvariant

Methods inherited from class Invariant

Methods inherited from class Object

Field Detail

debug

dkconfig_enabled

Constructor Detail

PairwiseIntLessEqual

PairwiseIntLessEqual

PairwiseIntLessEqual

Method Detail

get_proto

enabled

instantiate_ok

instantiate_dyn

isObviousStatically

isObviousDynamically

resurrect_done_swapped

swap_class

repr

getComparator

format_using

format_daikon

format_esc

format_simplify

format_java_family

format_csharp

check_modified

add_modified

computeConfidence

isSameFormula

isExclusiveFormula

find

get_ni_suppressions