daikon.inv.binary.sequenceScalar
Class SeqIntLessThan

Object
  Invariant
      BinaryInvariant
          SequenceScalar
              SeqIntLessThan

All Implemented Interfaces:

Serializable, Cloneable

public final class SeqIntLessThan
extends SequenceScalar

Represents an invariant between a long scalar and a a sequence of long values. Prints as x[] elements < y where x is a long sequence and y is a long scalar.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match

Field Summary

static Logger	debug
static boolean	dkconfig_enabled Boolean.

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, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Constructor Summary

protected	SeqIntLessThan()
protected	SeqIntLessThan(PptSlice ppt)

Method Summary

InvariantStatus	add_modified(long[] a, long x, int count) This method need not check for falsified; that is done by the caller.
InvariantStatus	check_modified(long[] a, long x, int count)
SeqIntLessThan	clone() Do nothing special, Overridden to remove exception from declaration
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 SeqIntLessThan	find(PptSlice ppt)
String	format_daikon()
String	format_esc()
String	format_java_family(OutputFormat format)
String	format_simplify()
String	format_using(OutputFormat format)
NISuppressionSet	get_ni_suppressions() Returns a list of non-instantiating suppressions for this invariant.
static SeqIntLessThan	get_proto() Returns the prototype invariant for SeqIntLessThan
protected SeqIntLessThan	instantiate_dyn(PptSlice slice) instantiates the invariant on the specified slice
boolean	instantiate_ok(VarInfo[] vis) Non-equal SeqIntComparison is only valid on integral types
boolean	isExact() Subclasses should override.
boolean	isExclusiveFormula(Invariant other)
DiscardInfo	isObviousDynamically(VarInfo[] vis) Checks to see if this is obvious over the specified variables.
DiscardInfo	isObviousStatically(VarInfo[] vis) Checks to see if the comparison is obvious statically.
boolean	isSameFormula(Invariant other)
String	repr() For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.

Methods inherited from class SequenceScalar

add_unmodified, add, check_unmodified, check, is_symmetric, resurrect_done_swapped, resurrect_done_unswapped, resurrect_done, scl_index, sclvar, sclvar, seq_first, seq_index, seqvar, seqvar, valid_types

Methods inherited from class BinaryInvariant

add_unordered, check_unordered, find, get_swap

Methods inherited from class Invariant

add_sample, asInvClass, clear_falsified, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enoughSamples, falsify, find, format_too_few_samples, format_unimplemented, format, formatFuzzy, get_comparability, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isInteresting, isObvious, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousDynamically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isObviousStatically, 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

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff SeqIntLessThan invariants should be considered.

debug

public static final Logger debug

Constructor Detail

SeqIntLessThan

protected SeqIntLessThan(PptSlice ppt)

SeqIntLessThan

protected SeqIntLessThan()

Method Detail

get_proto

public static SeqIntLessThan get_proto()

Returns the prototype invariant for SeqIntLessThan

enabled

public boolean enabled()

Returns whether or not this invariant is enabled

Overrides:

enabled in class Invariant

instantiate_ok

public boolean instantiate_ok(VarInfo[] vis)

Non-equal SeqIntComparison is only valid on integral types

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

instantiate_dyn

protected SeqIntLessThan instantiate_dyn(PptSlice slice)

instantiates the invariant on the specified slice

Overrides:

instantiate_dyn in class Invariant

Returns:

the new invariant

isObviousStatically

public DiscardInfo isObviousStatically(VarInfo[] vis)

Checks to see if the comparison is obvious statically. Makes the following checks

    max(A[]) op A[]
    min(A[]) op A[]
 

JHP: Note that these are not strict implications, these are merely uninteresting comparisons (except when op is GreaterEqual for max and LessEqual for min)

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.

clone

public SeqIntLessThan clone()

Description copied from class: Invariant

Do nothing special, Overridden to remove exception from declaration

Overrides:

clone in class Invariant

repr

public String repr()

Description copied from class: Invariant

For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.

Overrides:

repr in class Invariant

format_using

public String format_using(OutputFormat format)

Specified by:

format_using in class Invariant

format_daikon

public String format_daikon()

format_esc

public String format_esc()

format_simplify

public String format_simplify()

format_java_family

public String format_java_family(OutputFormat format)

check_modified

public InvariantStatus check_modified(long[] a,
                                      long x,
                                      int count)

Specified by:

check_modified in class SequenceScalar

add_modified

public InvariantStatus add_modified(long[] a,
                                    long x,
                                    int count)

Description copied from class: SequenceScalar

This method need not check for falsified; that is done by the caller.

Specified by:

add_modified in class SequenceScalar

computeConfidence

protected double computeConfidence()

Description copied from class: Invariant

This method computes the confidence that this invariant occurred by chance. Users should use getConfidence() instead.

Specified by:

computeConfidence in class Invariant

See Also:

Invariant.getConfidence()

isExact

public boolean isExact()

Description copied from class: Invariant

Subclasses should override. An exact invariant indicates that given all but one variable value, the last one can be computed. (I think that's correct, anyway.) Examples are IntComparison (when only equality is possible), LinearBinary, FunctionUnary. OneOf is treated differently, as an interface. The result of this method does not depend on whether the invariant is justified, destroyed, etc.

Overrides:

isExact in class Invariant

isSameFormula

public boolean isSameFormula(Invariant other)

Overrides:

isSameFormula in 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.

isExclusiveFormula

public boolean isExclusiveFormula(Invariant other)

Overrides:

isExclusiveFormula in 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.

find

public static SeqIntLessThan find(PptSlice ppt)

isObviousDynamically

public DiscardInfo isObviousDynamically(VarInfo[] vis)

Checks to see if this is obvious over the specified variables. Implements the following checks:

  (x op B[]) ^ (B[] subsequence A[]) ==> (x op A[])
  (A[] == [])                        ==> (x op A[])


Overrides:
isObviousDynamically in class Invariant

get_ni_suppressions

public NISuppressionSet get_ni_suppressions()

Returns a list of non-instantiating suppressions for this invariant.

Overrides:

get_ni_suppressions in class Invariant