Package daikon.inv

Class GuardingImplication

Object

Invariant

Joiner

Implication

GuardingImplication

All Implemented Interfaces:

Serializable, Cloneable

public class GuardingImplication
extends Implication

This is a special implication invariant that guards any invariants that are over variables that are sometimes missing. For example, if the invariant a.x = 0 is true, the guarded implication is a != null => a.x = 0.

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 inherited from class Implication

iff

Fields inherited from class Joiner

left, right

Fields inherited from class Invariant

checkedMergeOverridden, CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debug, 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
double	computeConfidence()	This method computes the confidence that this invariant occurred by chance.
boolean	enoughSamples()	Returns true if the invariant has enough samples to have its computed constants well-formed.
boolean	isWorthPrinting()
static GuardingImplication	makeGuardingImplication(PptTopLevel ppt, Invariant predicate, Invariant consequent, boolean iff)

Methods inherited from class Implication

consequent, enabled, format_using, hasUninterestingConstant, instantiate_dyn, isAllPrestate, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousStatically, isObviousStatically_SomeInEquality, isSameFormula, isSameInvariant, log, log, makeImplication, merge, predicate, repr, valid_types

Methods inherited from class Joiner

isObviousDerived, isObviousImplied, isValidEscExpression, 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, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, instantiate, instantiate_ok, is_false, is_ni_suppressed, isActive, isEqualityComparison, isExact, isExclusiveFormula, isObvious, isObviousDynamically, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isValidExpression, justified, logDetail, logOn, match, 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

Method Detail

makeGuardingImplication

public static GuardingImplication makeGuardingImplication(PptTopLevel ppt,
                                                          Invariant predicate,
                                                          Invariant consequent,
                                                          boolean iff)

isWorthPrinting

@Pure
public boolean isWorthPrinting()

Overrides:

isWorthPrinting in class Invariant

enoughSamples

public boolean enoughSamples(@GuardSatisfied GuardingImplication this)

Description copied from class: Invariant

Returns true if the invariant has enough samples to have its computed constants well-formed. Is overridden in classes like LinearBinary/Ternary and Upper/LowerBound.

Overrides:

enoughSamples in class Invariant

Returns:

true if the invariant has enough samples to have its computed constants well-formed

computeConfidence

public 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 Implication

Returns:

confidence of this invariant

See Also:

Invariant.getConfidence()