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

CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debug, 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

Method Summary

double	computeConfidence() This method computes the confidence that this invariant occurred by chance.
boolean	enoughSamples()
boolean	isWorthPrinting()
static GuardingImplication	makeGuardingImplication(PptTopLevel ppt, Invariant predicate, Invariant consequent, boolean iff)

Methods inherited from class Implication

consequent, format_using, hasUninterestingConstant, isAllPrestate, isInteresting, isObviousDynamically_SomeInEquality, isObviousDynamically, isObviousStatically_SomeInEquality, isObviousStatically, isSameFormula, isSameInvariant, log, log, makeImplication, predicate, repr

Methods inherited from class Joiner

isObviousDerived, isObviousImplied, isValidEscExpression, resurrect_done

Methods inherited from class Invariant

add_sample, asInvClass, clear_falsified, clone_and_permute, clone, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enabled, falsify, find, format_too_few_samples, format_unimplemented, format, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, instantiate_dyn, instantiate_ok, instantiate, is_false, is_ni_suppressed, isActive, isExact, isExclusiveFormula, isObvious, isObviousDynamically_SomeInEqualityHelper, isObviousDynamically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEqualityHelper, isObviousStatically, isReflexive, isValidExpression, justified, 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, valid_types, 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

public boolean isWorthPrinting()

Overrides:

isWorthPrinting in class Invariant

enoughSamples

public boolean enoughSamples()

Overrides:

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

computeConfidence

public double computeConfidence()

Description copied from class: Invariant

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

Overrides:

computeConfidence in class Implication

See Also:

Invariant.getConfidence()