Package daikon.inv.unary.sequence

Class SeqIndexFloatGreaterEqual

Object

Invariant

UnaryInvariant

SingleSequence

SingleFloatSequence

SeqIndexFloatGreaterEqual

All Implemented Interfaces:

Serializable, Cloneable

public class SeqIndexFloatGreaterEqual
extends SingleFloatSequence

Represents an invariant over sequences of double 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

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	SeqIndexFloatGreaterEqual(PptSlice slice)

Method Summary

Modifier and Type	Method	Description
InvariantStatus	add_modified(double @Interned [] a, int count)	Similar to SingleFloatSequence.check_modified(double[], int) except that it can change the state of the invariant if necessary.
InvariantStatus	check_modified(double @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 we are enabled
static @Nullable SeqIndexFloatGreaterEqual	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 SeqIndexFloatGreaterEqual
static SeqIndexFloatGreaterEqual	get_proto()	Returns the prototype invariant for SeqIndexFloatGreaterEqual
String	getComparator()
SeqIndexFloatGreaterEqual	instantiate_dyn(PptSlice slice)	Instantiate the invariant on the specified slice.
boolean	instantiate_ok(VarInfo[] vis)	Check that SeqIndex comparisons make sense over these vars.
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 SingleFloatSequence

add, add_unmodified, check, check_unmodified, valid_types

Methods inherited from class SingleSequence

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 SeqIndexFloatGreaterEqual invariants should be considered.

Constructor Detail

SeqIndexFloatGreaterEqual

protected SeqIndexFloatGreaterEqual(PptSlice slice)

Method Detail

get_proto

public static SeqIndexFloatGreaterEqual get_proto()

Returns the prototype invariant for SeqIndexFloatGreaterEqual

enabled

public boolean enabled()

returns whether or not we are enabled

Specified by:

enabled in class Invariant

instantiate_ok

public boolean instantiate_ok(VarInfo[] vis)

Check that SeqIndex comparisons make sense over these vars.

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

instantiate_dyn

public SeqIndexFloatGreaterEqual instantiate_dyn( SeqIndexFloatGreaterEqual this,
                                                 PptSlice slice)

Instantiate the invariant on the specified 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 SeqIndexFloatGreaterEqual

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 SeqIndexFloatGreaterEqual 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 SeqIndexFloatGreaterEqual this)

format_esc

public String format_esc(@GuardSatisfied SeqIndexFloatGreaterEqual this)

format_csharp_contract

public String format_csharp_contract(@GuardSatisfied SeqIndexFloatGreaterEqual this)

format_java_family

public String format_java_family(@GuardSatisfied SeqIndexFloatGreaterEqual this,
                                 OutputFormat format)

format_simplify

public String format_simplify(@GuardSatisfied SeqIndexFloatGreaterEqual this)

check_modified

public InvariantStatus check_modified(double @Interned [] a,
                                      int count)

Description copied from class: SingleFloatSequence

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 SingleFloatSequence

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(double @Interned [] a,
                                    int count)

Description copied from class: SingleFloatSequence

Similar to SingleFloatSequence.check_modified(double[], 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 SingleFloatSequence.check_modified(double[], int). This method need not check for falsification; that is done by the caller.

Specified by:

add_modified in class SingleFloatSequence

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 SeqIndexFloatGreaterEqual 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