daikon.inv
Class Implication

Object
  Invariant
      Joiner
          Implication

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

GuardingImplication

public class Implication
extends Joiner

The Implication invariant class is used internally within Daikon to handle invariants that are only true when certain other conditions are also true (splitting).

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

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

Field Summary

boolean

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

Constructor Summary

protected

Implication(PptSlice ppt, Invariant predicate, Invariant consequent, boolean iff, Invariant orig_predicate, Invariant orig_consequent)

Method Summary

protected double	computeConfidence() This method computes the confidence that this invariant occurred by chance.
Invariant	consequent()
String	format_using(OutputFormat format)
boolean	hasUninterestingConstant() This is the test that's planned to replace the poorly specified "isInteresting" check.
boolean	isAllPrestate()
boolean	isInteresting()
DiscardInfo	isObviousDynamically_SomeInEquality() Return true if the rightr side of the implication some equality combinations of its member variables are dynamically obvious.
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.
DiscardInfo	isObviousStatically_SomeInEquality() Return true if the right side of the implication and some equality combinations of its member variables are statically obvious.
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)
boolean	isSameInvariant(Invariant other)
void	log(Logger log, String msg) Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String).
boolean	log(String msg) Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String).
static Implication	makeImplication(PptTopLevel ppt, Invariant predicate, Invariant consequent, boolean iff, Invariant orig_predicate, Invariant orig_consequent) Creates a new Implication Invariant and adds it to the PptTopLevel.
Invariant	predicate()
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 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, enoughSamples, 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, isWorthPrinting, 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

Field Detail

iff

public boolean iff

Constructor Detail

Implication

protected Implication(PptSlice ppt,
                      Invariant predicate,
                      Invariant consequent,
                      boolean iff,
                      Invariant orig_predicate,
                      Invariant orig_consequent)

Method Detail

predicate

public Invariant predicate()

consequent

public Invariant consequent()

makeImplication

public static Implication makeImplication(PptTopLevel ppt,
                                          Invariant predicate,
                                          Invariant consequent,
                                          boolean iff,
                                          Invariant orig_predicate,
                                          Invariant orig_consequent)

Creates a new Implication Invariant and adds it to the PptTopLevel.

Returns:

null if predicate and the consequent are the same, or if the PptTopLevel already contains this Implication.

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()

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.

Specified by:

repr in class Joiner

format_using

public String format_using(OutputFormat format)

Specified by:

format_using in class Joiner

isObviousStatically

public 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

public 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

isObviousStatically_SomeInEquality

public DiscardInfo isObviousStatically_SomeInEquality()

Return true if the right side of the implication and some equality combinations of its member variables are statically obvious. For example, if a == b, and f(a) is obvious, then so is f(b). We use the someInEquality (or least interesting) method during printing so we only print an invariant if all its variables are interesting, since a single, static, non interesting occurance means all the equality combinations aren't interesting. This must be overridden for Implication because the right side is the invariant of interest. The standard version passes the vis from the slice containing the implication itself (slice 0).

Overrides:

isObviousStatically_SomeInEquality in class Invariant

Returns:

the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

isObviousDynamically_SomeInEquality

public DiscardInfo isObviousDynamically_SomeInEquality()

Return true if the rightr side of the implication some equality combinations of its member variables are dynamically obvious. For example, a == b, and f(a) is obvious, so is f(b). We use the someInEquality (or least interesting) method during printing so we only print an invariant if all its variables are interesting, since a single, dynamic, non interesting occurance means all the equality combinations aren't interesting. This must be overridden for Implication because the right side is the invariant of interest. The standard version passes the vis from the slice containing the implication itself (slice 0).

Overrides:

isObviousDynamically_SomeInEquality in class Invariant

Returns:

the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

isSameFormula

public boolean isSameFormula(Invariant other)

Overrides:

isSameFormula in class Joiner

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.

isSameInvariant

public boolean isSameInvariant(Invariant other)

Overrides:

isSameInvariant in class Joiner

Returns:

true iff the argument is the "same" invariant as this. Same, in this case, means a matching type, formula, and variable names.

isInteresting

public boolean isInteresting()

Overrides:

isInteresting in class Joiner

hasUninterestingConstant

public boolean hasUninterestingConstant()

Description copied from class: Invariant

This is the test that's planned to replace the poorly specified "isInteresting" check. In the future, the set of interesting constants might be determined by a static analysis of the source code, but for the moment, we only consider -1, 0, 1, and 2 as interesting. Intuitively, the justification for this test is that an invariant that includes an uninteresting constant (say, "size(x[]) < 237") is likely to be an artifact of the way the program was tested, rather than a statement that would in fact hold over all possible executions.

Overrides:

hasUninterestingConstant in class Invariant

isAllPrestate

public boolean isAllPrestate()

Overrides:

isAllPrestate in class Invariant

Returns:

true if this invariant is only over prestate variables .

log

public void log(Logger log,
                String msg)

Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String). Uses the consequent as the logger

Overrides:

log in class Invariant

log

public boolean log(String msg)

Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String). Uses the consequent as the logger

Returns:

whether or not it logged anything