Package daikon.inv.binary.twoScalar

Class FloatGreaterEqual

Object

Invariant

BinaryInvariant

TwoFloat

FloatGreaterEqual

All Implemented Interfaces:

Serializable, Cloneable

public final class FloatGreaterEqual
extends TwoFloat

Represents an invariant of ≥ between two double scalars. 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
static boolean	dkconfig_enabled	Boolean.

Fields inherited from class TwoFloat

swap

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

Method Summary

Modifier and Type	Method	Description
InvariantStatus	add(@Interned Object v1, @Interned Object v2, int mod_index, int count)
InvariantStatus	add_modified(double v1, double v2, int count)	Default implementation simply calls check.
InvariantStatus	check_modified(double v1, double v2, 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 FloatGreaterEqual	find(PptSlice ppt)
String	format_using(OutputFormat format)	Return a printed representation of this invariant, in the given format.
NISuppressionSet	get_ni_suppressions()	Returns the non-instantiating suppressions for this invariant.
static FloatGreaterEqual	get_proto()	Returns the prototype invariant for FloatGreaterEqual.
protected FloatGreaterEqual	instantiate_dyn(PptSlice slice)	Instantiates (creates) an invariant of the same class on the specified slice.
boolean	instantiate_ok(VarInfo[] vis)	Returns whether or not the specified var types are valid for FloatGreaterEqual.
boolean	isExact()	Subclasses should override.
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<? extends Invariant>	swap_class()	Returns the class that corresponds to this class with its variable order swapped.

Methods inherited from class TwoFloat

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

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff FloatGreaterEqual invariants should be considered.

debug

public static final Logger debug

Method Detail

get_proto

public static FloatGreaterEqual get_proto()

Returns the prototype invariant for FloatGreaterEqual.

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)

Returns whether or not the specified var types are valid for FloatGreaterEqual.

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

instantiate_dyn

protected FloatGreaterEqual instantiate_dyn( FloatGreaterEqual 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

resurrect_done_swapped

protected Invariant resurrect_done_swapped()

Description copied from class: TwoFloat

Swaps the variables by inverting the state of swap.

Overrides:

resurrect_done_swapped in class TwoFloat

swap_class

public static Class<? extends Invariant> swap_class()

Returns the class that corresponds to this class with its variable order swapped.

find

public static @Nullable FloatGreaterEqual find(PptSlice ppt)

repr

public String repr(@GuardSatisfied FloatGreaterEqual this)

Description copied from class: TwoFloat

Returns a representation of the class. This includes the classname, variables, and swap state.

Overrides:

repr in class TwoFloat

Returns:

a string representation of this

format_using

@SideEffectFree
public String format_using(@GuardSatisfied FloatGreaterEqual 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

check_modified

public InvariantStatus check_modified(double v1,
                                      double v2,
                                      int count)

Description copied from class: TwoFloat

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 TwoFloat

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 v1,
                                    double v2,
                                    int count)

Description copied from class: TwoFloat

Default implementation simply calls check. Subclasses can override.

Overrides:

add_modified in class TwoFloat

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 TwoFloat

Returns:

confidence of this invariant

See Also:

Invariant.getConfidence()

isExact

@Pure
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

Returns:

true if any variable value can be computed from all the others

add

public InvariantStatus add(@Interned Object v1,
                           @Interned Object v2,
                           int mod_index,
                           int count)

Overrides:

add in class TwoFloat

isSameFormula

@Pure
public boolean isSameFormula(Invariant other)

Description copied from class: TwoFloat

Return true if both invariants are the same class and the order of the variables (swap) is the same.

Overrides:

isSameFormula in class TwoFloat

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

isObviousStatically

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

get_ni_suppressions

@Pure
public NISuppressionSet get_ni_suppressions()

Returns the non-instantiating suppressions for this invariant.

Overrides:

get_ni_suppressions in class Invariant

Returns:

the set of non-instantiating suppressions for this invariant