Object
- Invariant

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

BinaryInvariant, DiffDummyInvariant, DummyInvariant, Equality, Joiner, TernaryInvariant, UnaryInvariant
```
@UsesObjectEquals
public abstract class Invariant
extends Object
implements Serializable, Cloneable
```
Base implementation for Invariant objects. Intended to be subclassed but not to be directly instantiated. Rules/assumptions for invariants:
For each program point's set of VarInfos, there exists no more than one invariant of its type. For example, between variables a and b at PptTopLevel T, there will not be two instances of invariant I(a, b).

See Also:

Serialized Form

Nested Class Summary

Nested Classes
Modifier and Type	Class	Description
`static class`	`Invariant.ClassVarnameComparator`
`static class`	`Invariant.ClassVarnameFormulaComparator`	Orders invariants by class, then variable names, then formula.
`static class`	`Invariant.InvariantComparatorForPrinting`	Compare based on arity, then printed representation.
`static class`	`Invariant.Match`	Class used as a key to store invariants in a MAP where their equality depends on the invariant representing the same invariant (i.e., their class is the same) and the same internal state (when multiple invariants with the same class are possible)

Field Summary

Fields
Modifier and Type	Field	Description
`static double`	`CONFIDENCE_JUSTIFIED`	The probability that this could have happened by chance alone.
`static double`	`CONFIDENCE_NEVER`	-1 = delete this invariant; we know it's not true
`static double`	`CONFIDENCE_UNJUSTIFIED`	(0..1) = greater to lesser likelihood of coincidence 0 = must have happened by chance
`static Logger`	`debug`	General debug tracer.
`static Logger`	`debugFlow`	Debug tracer for invariant flow.
`static Logger`	`debugGuarding`	Debug tracer for guarding.
`static Logger`	`debugIsObvious`	Debug tracer for isObvious checks.
`static Logger`	`debugIsWorthPrinting`	Debug tracer for isWorthPrinting() checks.
`static Logger`	`debugPrint`	Debug tracer for printing invariants.
`static Logger`	`debugPrintEquality`	Debug tracer for printing equality invariants.
`static double`	`dkconfig_confidence_limit`	Floating-point number between 0 and 1.
`static double`	`dkconfig_fuzzy_ratio`	Floating-point number between 0 and 0.1, representing the maximum relative difference between two floats for fuzzy comparisons.
`static boolean`	`dkconfig_simplify_define_predicates`	A boolean value.
`protected boolean`	`falsified`	True exactly if the invariant has been falsified: it is guaranteed never to hold (and should be either in the process of being destroyed or about to be destroyed).
`static boolean`	`invariantEnabledDefault`	The default for dkconfig_enabled in each subclass of Invariant.
`boolean`	`isGuardingPredicate`
`static int`	`min_mod_non_missing_samples`	At least this many samples are required, or else we don't report any invariant at all.
`PptSlice`	`ppt`	The program point for this invariant; includes values, number of samples, VarInfos, etc.
`static double`	`PROBABILITY_JUSTIFIED`	The probability that this could have happened by chance alone.
`static double`	`PROBABILITY_NEVER`	3 = delete this invariant; we know it's not true
`static double`	`PROBABILITY_UNJUSTIFIED`	(0..1) = lesser to greater likelihood of coincidence 1 = must have happened by chance

Constructor Summary

Constructors
Modifier Constructor Description

protected Invariant()

protected Invariant(PptSlice ppt)

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`InvariantStatus`	`add_sample(ValueTuple vt, int count)`	Adds the specified sample to the invariant and returns the result.
`static Class<? extends Invariant>`	`asInvClass(Object x)`
`void`	`checkRep()`	Throws an exception if this object is invalid.
`void`	`clear_falsified()`	Clear the falsified flag.
`Invariant`	`clone()`	Do nothing special, Overridden to remove exception from declaration.
`Invariant`	`clone_and_permute(int[] permutation)`	Clones the invariant and then permutes it as specified.
`protected abstract double`	`computeConfidence()`	This method computes the confidence that this invariant occurred by chance.
`static double`	`conf_is_ge(double x, double goal)`	Return Invariant.CONFIDENCE_JUSTIFIED if x≥goal.
`static double`	`confidence_and(double c1, double c2)`	Return the "and" of the given confidences.
`static double`	`confidence_and(double c1, double c2, double c3)`	Return the "and" of the given confidences.
`static double`	`confidence_or(double c1, double c2)`	Return the "or" of the given confidences.
`@Nullable Invariant`	`createGuardedInvariant(boolean install)`	This procedure guards one invariant and returns the resulting guarded invariant (implication), without placing it in any slice and without modifying the original invariant.
`@Nullable Invariant`	`createGuardingPredicate(boolean install)`	Create a guarding predicate for a given invariant.
`abstract boolean`	`enabled()`	Returns whether or not this class of invariants is currently enabled.
`boolean`	`enoughSamples()`	Returns true if the invariant has enough samples to have its computed constants well-formed.
`void`	`falsify()`	Marks the invariant as falsified.
`static @Nullable Invariant`	`find(Class<? extends Invariant> invclass, PptSlice ppt)`	Look up a previously instantiated Invariant.
`String`	`format()`	Returns a high-level printed representation of the invariant, for user output.
`String`	`format_classname()`	Returns the class name of the invariant, for use in debugging output.
`String`	`format_too_few_samples(OutputFormat format, @Nullable String attempt)`	Returns standard "too few samples for to have interesting invariant" for the requested format.
`String`	`format_unimplemented(OutputFormat format)`	Returns standard "format needs to be implemented" for the given requested format.
`abstract String`	`format_using(OutputFormat format)`	Return a printed representation of this invariant, in the given format.
`static String`	`formatFuzzy(String method, VarInfo v1, VarInfo v2, OutputFormat format)`	Used throughout Java family formatting of invariants.
`VarComparability`	`get_comparability()`	Returns a single VarComparability that describes the set of variables used by this invariant.
`@Nullable NISuppressionSet`	`get_ni_suppressions()`	Returns the set of non-instantiating suppressions for this invariant.
`double`	`getConfidence()`	Given that this invariant has been true for all values seen so far, this method returns the confidence that that situation has occurred by chance alone.
`List<VarInfo>`	`getGuardingList()`	Return a list of all the variables that must be non-null in order for this invariant to be evaluated.
`static List<VarInfo>`	`getGuardingList(VarInfo[] varInfos)`	Returns the union of calling VarInfo.getGuardingList on each element of the argument.
`boolean`	`hasUninterestingConstant()`	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.
`@Nullable Invariant`	`instantiate(PptSlice slice)`	Instantiates this invariant over the specified slice.
`protected abstract Invariant`	`instantiate_dyn(PptSlice slice)`	Instantiates (creates) an invariant of the same class on the specified slice.
`boolean`	`instantiate_ok(VarInfo[] vis)`	Returns true if it makes sense to instantiate this invariant over the specified variables.
`boolean`	`is_false()`	Returns whether or not this invariant has been falsified.
`boolean`	`is_ni_suppressed()`	Returns whether or not this invariant is ni-suppressed.
`boolean`	`isActive()`	Returns whether or not the invariant is currently active.
`boolean`	`isAllPrestate()`	Returns true if this invariant is only over prestate variables.
`boolean`	`isEqualityComparison()`	Returns true if this is an equality comparison.
`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`	`isObvious()`	Return true if this invariant is necessarily true from a fact that can be determined statically (i.e., the decls files) or dynamically (after checking data).
`@Nullable DiscardInfo`	`isObviousDynamically()`	Return true if this invariant is necessarily true from a fact that can be determined dynamically (after checking data, based on other invariants that were inferred).
`@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`	`isObviousDynamically_SomeInEquality()`	Return true if this invariant and some equality combinations of its member variables are dynamically obvious.
`protected @Nullable DiscardInfo`	`isObviousDynamically_SomeInEqualityHelper(VarInfo[] vis, VarInfo[] assigned, int position)`	Recurse through vis (an array of leaders) and generate the cartesian product of their equality sets; in other words, every combination of one element from each equality set.
`@Nullable DiscardInfo`	`isObviousStatically()`	Return true if this invariant is necessarily true from a fact that can be determined statically from the decls files.
`@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`	`isObviousStatically_AllInEquality()`	Return true if this invariant and all equality combinations of its member variables are necessarily true from a fact that can be determined statically (i.e., the decls files).
`@Nullable DiscardInfo`	`isObviousStatically_SomeInEquality()`	Return true if this invariant and some equality combinations of its member variables are statically obvious.
`protected @Nullable DiscardInfo`	`isObviousStatically_SomeInEqualityHelper(VarInfo[] vis, VarInfo[] assigned, int position)`	Recurse through vis and generate the cartesian product of ...
`boolean`	`isReflexive()`	Return true if more than one of the variables in the invariant are the same variable.
`abstract boolean`	`isSameFormula(Invariant other)`	Returns true iff the two invariants represent the same mathematical formula.
`boolean`	`isSameInvariant(Invariant inv2)`	Returns true iff the argument is the "same" invariant as this.
`boolean`	`isValidEscExpression()`	Returns a conjuction of mapping the same function of our expresssions's VarInfos, in general.
`boolean`	`isValidExpression(OutputFormat format)`	Returns true if this Invariant can be properly formatted for the given output format.
`boolean`	`isWorthPrinting()`
`boolean`	`justified()`	A wrapper around getConfidence() or getConfidence().
`boolean`	`log(String format, @Nullable Object... args)`	Logs a description of the invariant and the specified msg via the logger as described in `daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String)`.
`void`	`log(Logger log, String msg)`	Logs a description of the invariant and the specified msg via the logger as described in `daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String)`.
`static boolean`	`logDetail()`	Returns true if detailed logging is on.
`static boolean`	`logOn()`	Returns whether or not logging is on.
`boolean`	`match(Invariant inv)`	Returns whether or not two invariants are of the same type.
`@Nullable Invariant`	`merge(List<Invariant> invs, PptSlice parent_ppt)`	Merge the invariants in invs to form a new invariant.
`boolean`	`mergeFormulasOk()`	Returns whether or not it is possible to merge invariants of the same class but with different formulas when combining invariants from lower ppts to build invariants at upper program points.
`Invariant`	`permute(int[] permutation)`	Permutes the invariant as specified.
`static double`	`prob_and(double p1, double p2)`	Return the "and" of the given probabilities.
`static double`	`prob_and(double p1, double p2, double p3)`	Return the "and" of the given probabilities.
`static double`	`prob_is_ge(double x, double goal)`	Return Invariant.PROBABILITY_JUSTIFIED if x≥goal.
`static double`	`prob_or(double p1, double p2)`	Return the "or" of the given probabilities.
`void`	`repCheck()`	Check the rep invariants of this.
`String`	`repr()`	For printing invariants, there are two interfaces: repr gives a low-level representation (`repr_prob()` also prints the confidence), and `format()` gives a high-level representation for user output.
`String`	`repr_prob()`	For printing invariants, there are two interfaces: `repr()` gives a low-level representation (repr_prob also prints the confidence), and `format()` gives a high-level representation for user output.
`Invariant`	`resurrect(PptSlice new_ppt, int[] permutation)`	Take a falsified invariant and resurrect it in a new PptSlice.
`protected abstract Invariant`	`resurrect_done(int[] permutation)`	Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.
`static String`	`simplify_format_double(double d)`	Convert a floating point value into the weird Modula-3-like floating point format that the Simplify tool requires.
`static String`	`simplify_format_long(long l)`	Conver a long integer value into a format that Simplify can use.
`static String`	`simplify_format_string(String s)`	Convert a string value into the weird \|-quoted format that the Simplify tool requires.
`boolean`	`state_match(Object state)`	Returns whether or not the invariant matches the specified state.
`String`	`toString()`
`static String`	`toString(Invariant[] invs)`	Return a string representation of the given invariants.
`Invariant`	`transfer(PptSlice new_ppt, int[] permutation)`	Make a copy of this invariant and transfer it into a new PptSlice.
`boolean`	`usesVar(VarInfo vi)`	Return true if this invariant uses the given variable.
`boolean`	`usesVar(String name)`	Return true if this invariant uses the given variable.
`boolean`	`usesVarDerived(String name)`	Return true if this invariant uses the given variable or any variable derived from it.
`abstract boolean`	`valid_types(VarInfo[] vis)`	Returns whether or not the invariant is valid over the basic types in vis.
`String`	`varNames()`	Return a string representation of the variable names.

Methods inherited from class Object
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - debug
```
public static final Logger debug
```
    General debug tracer.
  - debugPrint
```
public static final Logger debugPrint
```
    Debug tracer for printing invariants.
  - debugFlow
```
public static final Logger debugFlow
```
    Debug tracer for invariant flow.
  - debugPrintEquality
```
public static final Logger debugPrintEquality
```
    Debug tracer for printing equality invariants.
  - debugIsWorthPrinting
```
public static final Logger debugIsWorthPrinting
```
    Debug tracer for isWorthPrinting() checks.
  - debugGuarding
```
public static final Logger debugGuarding
```
    Debug tracer for guarding.
  - debugIsObvious
```
public static final Logger debugIsObvious
```
    Debug tracer for isObvious checks.
  - dkconfig_confidence_limit
```
public static double dkconfig_confidence_limit
```
    Floating-point number between 0 and 1. Invariants are displayed only if the confidence that the invariant did not occur by chance is greater than this. (May also be set via the --conf_limit command-line option to Daikon; refer to manual.)
  - dkconfig_simplify_define_predicates
```
public static boolean dkconfig_simplify_define_predicates
```
    A boolean value. If true, Daikon's Simplify output (printed when the --format simplify flag is enabled, and used internally by --suppress_redundant) will include new predicates representing some complex relationships in invariants, such as lexical ordering among sequences. If false, some complex relationships will appear in the output as complex quantified formulas, while others will not appear at all. When enabled, Simplify may be able to make more inferences, allowing --suppress_redundant to suppress more redundant invariants, but Simplify may also run more slowly.
  - dkconfig_fuzzy_ratio
```
public static double dkconfig_fuzzy_ratio
```
    Floating-point number between 0 and 0.1, representing the maximum relative difference between two floats for fuzzy comparisons. Larger values will result in floats that are relatively farther apart being treated as equal. A value of 0 essentially disables fuzzy comparisons. Specifically, if abs(1 - f1/f2) is less than or equal to this value, then the two doubles (f1 and f2) will be treated as equal by Daikon.
  - invariantEnabledDefault
```
public static boolean invariantEnabledDefault
```
    The default for dkconfig_enabled in each subclass of Invariant.
  - ppt
```
@Unused(when=Prototype.class)
public PptSlice ppt
```
    The program point for this invariant; includes values, number of samples, VarInfos, etc. Can be null for a "prototype" invariant.
  - falsified
```
protected boolean falsified
```
    True exactly if the invariant has been falsified: it is guaranteed never to hold (and should be either in the process of being destroyed or about to be destroyed). This should never be set directly; instead, call destroy().
  - isGuardingPredicate
```
public boolean isGuardingPredicate
```
  - CONFIDENCE_JUSTIFIED
```
public static final double CONFIDENCE_JUSTIFIED
```
    The probability that this could have happened by chance alone.
    1 = could never have happened by chance; that is, we are fully confident that this invariant is a real invariant
    
    See Also:
    
    Constant Field Values
  - CONFIDENCE_UNJUSTIFIED
```
public static final double CONFIDENCE_UNJUSTIFIED
```
    (0..1) = greater to lesser likelihood of coincidence
    0 = must have happened by chance
    
    See Also:
    
    Constant Field Values
  - CONFIDENCE_NEVER
```
public static final double CONFIDENCE_NEVER
```
    -1 = delete this invariant; we know it's not true
    
    See Also:
    
    Constant Field Values
  - PROBABILITY_JUSTIFIED
```
public static final double PROBABILITY_JUSTIFIED
```
    The probability that this could have happened by chance alone.
    0 = could never have happened by chance; that is, we are fully confident that this invariant is a real invariant
    
    See Also:
    
    Constant Field Values
  - PROBABILITY_UNJUSTIFIED
```
public static final double PROBABILITY_UNJUSTIFIED
```
    (0..1) = lesser to greater likelihood of coincidence
    1 = must have happened by chance
    
    See Also:
    
    Constant Field Values
  - PROBABILITY_NEVER
```
public static final double PROBABILITY_NEVER
```
    3 = delete this invariant; we know it's not true
    
    See Also:
    
    Constant Field Values
  - min_mod_non_missing_samples
```
public static final int min_mod_non_missing_samples
```
    At least this many samples are required, or else we don't report any invariant at all. (Except that OneOf invariants are treated differently.)
    
    See Also:
    
    Constant Field Values
- Constructor Detail
  - Invariant
```
protected Invariant(PptSlice ppt)
```
  - Invariant
```
protected Invariant()
```
- Method Detail
  - conf_is_ge
```
public static final double conf_is_ge(double x,
                                      double goal)
```
    Return Invariant.CONFIDENCE_JUSTIFIED if x≥goal. Return Invariant.CONFIDENCE_UNJUSTIFIED if x≤1. For intermediate inputs, the result gives confidence that grades between the two extremes. See the discussion of gradual vs. sudden confidence transitions.
    
    Parameters:
    
    x - the greater value
    
    goal - the lesser value
    
    Returns:
    
    CONFIDENCE_JUSTIFIED if x≥goal, Invariant.CONFIDENCE_UNJUSTIFIED if x≤1, other values otherwise
  - prob_is_ge
```
public static final double prob_is_ge(double x,
                                      double goal)
```
    Return Invariant.PROBABILITY_JUSTIFIED if x≥goal. Return Invariant.PROBABILITY_UNJUSTIFIED if x≤1. For intermediate inputs, the result gives probability that grades between the two extremes. See the discussion of gradual vs. sudden probability transitions.
    
    Parameters:
    
    x - the greater value
    
    goal - the lesser value
    
    Returns:
    
    if x≥goal: invariant.PROBABILITY_JUSTIFIED; if x≤1: Invariant.PROBABILITY_UNJUSTIFIED; otherwise: other values
  - confidence_and
```
public static final double confidence_and(double c1,
                                          double c2)
```
    Return the "and" of the given confidences. This is the confidence that multiple conditions (whose confidences are given) are all satisfied.
    
    Parameters:
    
    c1 - the confidence of the first condition
    
    c2 - the confidence of the second condition
    
    Returns:
    
    the "and" of the two condidences
  - confidence_and
```
public static final double confidence_and(double c1,
                                          double c2,
                                          double c3)
```
    Return the "and" of the given confidences. This is the confidence that multiple conditions (whose confidences are given) are all satisfied.
    
    Parameters:
    
    c1 - the confidence of the first condition
    
    c2 - the confidence of the second condition
    
    c3 - the confidence of the third condition
    
    Returns:
    
    the "and" of the two condidences
  - confidence_or
```
public static final double confidence_or(double c1,
                                         double c2)
```
    Return the "or" of the given confidences. This is the confidence that at least one of multiple conditions (whose confidences are given) is satisfied.
    
    Parameters:
    
    c1 - the confidence of the first condition
    
    c2 - the confidence of the second condition
    
    Returns:
    
    the "or" of the two condidences
  - prob_and
```
public static final double prob_and(double p1,
                                    double p2)
```
    Return the "and" of the given probabilities. This is the probability that multiple conditions (whose probabilities are given) are all satisfied.
    
    Parameters:
    
    p1 - the probability of the first condition
    
    p2 - the probability of the second condition
    
    Returns:
    
    the "and" of the two condidences
  - prob_and
```
public static final double prob_and(double p1,
                                    double p2,
                                    double p3)
```
    Return the "and" of the given probabilities. This is the probability that multiple conditions (whose probabilities are given) are all satisfied.
    
    Parameters:
    
    p1 - the probability of the first condition
    
    p2 - the probability of the second condition
    
    p3 - the probability of the third condition
    
    Returns:
    
    the "and" of the two condidences
  - prob_or
```
public static final double prob_or(double p1,
                                   double p2)
```
    Return the "or" of the given probabilities. This is the probability that at least one of multiple conditions (whose probabilities are given) is satisfied.
    
    Parameters:
    
    p1 - the probability of the first condition
    
    p2 - the probability of the second condition
    
    Returns:
    
    the "or" of the two condidences
  - enoughSamples
```
public boolean enoughSamples(@GuardSatisfied Invariant this)
```
    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.
    
    Returns:
    
    true if the invariant has enough samples to have its computed constants well-formed
  - justified
```
public final boolean justified( Invariant this)
```
    A wrapper around getConfidence() or getConfidence().
    
    Returns:
    
    true if this invariant's confidence is greater than the global confidence limit
  - getConfidence
```
public final double getConfidence( Invariant this)
```
    Given that this invariant has been true for all values seen so far, this method returns the confidence that that situation has occurred by chance alone.
    Returns the probability that the observed data did not happen by chance alone. The result is a value between 0 and 1 inclusive. 0 means that this invariant could never have occurred by chance alone; we are fully confident that its truth is no coincidence. 1 means that the invariant is certainly a happenstance, so the truth of the invariant is not relevant and it should not be reported. Values between 0 and 1 give differing confidences in the invariant. The method may also return CONFIDENCE_NEVER, meaning the invariant has been falsified.
    An invariant is printed only if its probability of not occurring by chance alone is large enough (by default, greater than .99; see Daikon's --conf_limit command-line option.
    As an example, consider the invariant "x!=0". If only one value, 22, has been seen for x, then the conclusion "x!=0" is not justified. But if there have been 1,000,000 values, and none of them were 0, then we may be confident that the property "x!=0" is not a coincidence.
    This method is a wrapper around computeConfidence(), which does the actual work.
    Consider the invariant is 'x is even', which has a 50% chance of being true by chance for each sample. Then a reasonable body for computeConfidence() would be
    return 1 - Math.pow(.5, ppt.num_samples());
    If 5 values had been seen, then this implementation would return 31/32, which is the likelihood that all 5 values seen so far were even not purely by chance.
    Returns:
    
    confidence of this invariant
    
    See Also:
    
    computeConfidence()
  - computeConfidence
```
protected abstract double computeConfidence( Invariant this)
```
    This method computes the confidence that this invariant occurred by chance. Clients should call getConfidence() instead.
    This method need not check the value of field "falsified", as the caller does that.
    
    Returns:
    
    confidence of this invariant
    
    See Also:
    
    getConfidence()
  - isExact
```
@Pure
public boolean isExact( Invariant this)
```
    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.
    
    Returns:
    
    true if any variable value can be computed from all the others
  - falsify
```
public void falsify( Invariant this)
```
    Marks the invariant as falsified. Should always be called rather than just setting the flag so that we can track when this happens.
  - clear_falsified
```
public void clear_falsified( Invariant this)
```
    Clear the falsified flag.
  - is_false
```
@Pure
public boolean is_false( Invariant this)
```
    Returns whether or not this invariant has been falsified.
    
    Returns:
    
    true if this invariant has been falsified
  - clone
```
@SideEffectFree
public Invariant clone(@GuardSatisfied Invariant this)
```
    Do nothing special, Overridden to remove exception from declaration.
    
    Overrides:
    
    clone in class Object
  - transfer
```
public Invariant transfer( Invariant this,
                          PptSlice new_ppt,
                          int[] permutation)
```
    Make a copy of this invariant and transfer it into a new PptSlice.
    
    Parameters:
    
    new_ppt - must have the same arity and types
    
    permutation - gives the varinfo array index mapping in the new ppt
    
    Returns:
    
    a copy of the invariant, on a different slice
  - clone_and_permute
```
public Invariant clone_and_permute( Invariant this,
                                   int[] permutation)
```
    Clones the invariant and then permutes it as specified. Normally used to make child invariant match the variable order of the parent when merging invariants bottom up.
  - resurrect
```
public Invariant resurrect( Invariant this,
                           PptSlice new_ppt,
                           int[] permutation)
```
    Take a falsified invariant and resurrect it in a new PptSlice.
    
    Parameters:
    
    new_ppt - must have the same arity and types
    
    permutation - gives the varinfo array index mapping
    
    Returns:
    
    the resurrected invariant, in a new PptSlice
  - get_comparability
```
public VarComparability get_comparability( Invariant this)
```
    Returns a single VarComparability that describes the set of variables used by this invariant. Since all of the variables in an invariant must be comparable, this can usually be the comparability information for any variable. The exception is when one or more variables is always comparable (comparable to everything else). An always comparable VarComparability is returned only if all of the variables involved are always comparable. Otherwise the comparability information from one of the non always-comparable variables is returned.
    
    Returns:
    
    a VarComparability that describes any (and all) of this invariant's variables
  - merge
```
public @Nullable Invariant merge( Invariant this,
                                 List<Invariant> invs,
                                 PptSlice parent_ppt)
```
    Merge the invariants in invs to form a new invariant. This implementation merely returns a clone of the first invariant in the list. This is correct for simple invariants whose equation or statistics don't depend on the actual samples seen. It should be overriden for more complex invariants (eg, bound, oneof, linearbinary, etc).
    
    Parameters:
    
    invs - list of invariants to merge. The invariants must all be of the same type and should come from the children of parent_ppt. They should also all be permuted to match the variable order in parent_ppt.
    
    parent_ppt - slice that will contain the new invariant
    
    Returns:
    
    the merged invariant or null if the invariants didn't represent the same invariant
  - permute
```
public Invariant permute( Invariant this,
                         int[] permutation)
```
    Permutes the invariant as specified. Often creates a new invariant (with a different class).
    
    Parameters:
    
    permutation - the permutation
    
    Returns:
    
    the permuted invariant
  - resurrect_done
```
protected abstract Invariant resurrect_done( Invariant this,
                                            int[] permutation)
```
    Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.
    
    Parameters:
    
    permutation - the permutation
    
    Returns:
    
    the permuted invariant
  - usesVar
```
public boolean usesVar( Invariant this,
                       VarInfo vi)
```
    Return true if this invariant uses the given variable.
  - usesVar
```
public boolean usesVar( Invariant this,
                       String name)
```
    Return true if this invariant uses the given variable.
  - usesVarDerived
```
public boolean usesVarDerived( Invariant this,
                              String name)
```
    Return true if this invariant uses the given variable or any variable derived from it.
  - varNames
```
public final String varNames(@GuardSatisfied Invariant this)
```
    Return a string representation of the variable names.
    
    Returns:
    
    a string representation of the variable names
  - repr
```
public String repr(@GuardSatisfied Invariant this)
```
    For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prob() also prints the confidence), and format() gives a high-level representation for user output.
    
    Returns:
    
    a string representation of this
  - repr_prob
```
public String repr_prob( Invariant this)
```
    For printing invariants, there are two interfaces: repr() gives a low-level representation (repr_prob also prints the confidence), and format() gives a high-level representation for user output.
    
    Returns:
    
    repr(), but with the confidence as well
  - format
```
@SideEffectFree
public String format(@GuardSatisfied Invariant this)
```
    Returns a high-level printed representation of the invariant, for user output. format produces normal output, while the repr() formatting routine produces low-level, detailed output for debugging, and repr_prob() also prints the confidence.
    
    Returns:
    
    a string representation of this
  - format_classname
```
public String format_classname()
```
    Returns the class name of the invariant, for use in debugging output. Returns "" if PrintInvariants.dkconfig_print_inv_class is false.
    
    Returns:
    
    a string representation of the class name of the invariant, or ""
  - format_using
```
@SideEffectFree
public abstract String format_using(@GuardSatisfied Invariant this,
                                    OutputFormat format)
```
    Return a printed representation of this invariant, in the given format.
  - isValidEscExpression
```
@Pure
public boolean isValidEscExpression( Invariant this)
```
    Returns a conjuction of mapping the same function of our expresssions's VarInfos, in general. Subclasses may override if they are able to handle generally-inexpressible properties in special-case ways.
    
    Returns:
    
    conjuction of mapping the same function of our expresssions's VarInfos
    
    See Also:
    
    VarInfo.isValidEscExpression()
  - isValidExpression
```
@Pure
public boolean isValidExpression( Invariant this,
                                 OutputFormat format)
```
    Returns true if this Invariant can be properly formatted for the given output format.
    
    Parameters:
    
    format - the expected output format
    
    Returns:
    
    true if this Invariant can be properly formatted for the given output format
  - format_unimplemented
```
public String format_unimplemented(@GuardSatisfied Invariant this,
                                   OutputFormat format)
```
    Returns standard "format needs to be implemented" for the given requested format. Made public so cores can call it.
    
    Parameters:
    
    format - the requested output format
    
    Returns:
    
    standard "format needs to be implemented" for the given requested format
  - format_too_few_samples
```
public String format_too_few_samples(@GuardSatisfied Invariant this,
                                     OutputFormat format,
                                     @Nullable String attempt)
```
    Returns standard "too few samples for to have interesting invariant" for the requested format. For machine-readable formats, this is just "true". An optional string argument, if supplied, is a human-readable description of the invariant in its uninformative state, which will be added to the message.
    
    Parameters:
    
    format - the requested output format
    
    Returns:
    
    standard "too few samples for to have interesting invariant" for the requested format
  - simplify_format_double
```
public static String simplify_format_double(double d)
```
    Convert a floating point value into the weird Modula-3-like floating point format that the Simplify tool requires.
    
    Parameters:
    
    d - the number to print
    
    Returns:
    
    a printed representation of the number, for Simplify
  - simplify_format_long
```
public static String simplify_format_long(long l)
```
    Conver a long integer value into a format that Simplify can use. If the value is too big, we have to print it in a weird way, then tell Simplify about its properties specially.
    
    Parameters:
    
    l - the number to print
    
    Returns:
    
    a printed representation of the number, for Simplify
  - simplify_format_string
```
public static String simplify_format_string(String s)
```
    Convert a string value into the weird |-quoted format that the Simplify tool requires. (Note that Simplify doesn't distinguish between variables, symbolic constants, and strings, so we prepend "_string_" to avoid collisions with variables and other symbols).
    
    Parameters:
    
    s - the number to print
    
    Returns:
    
    a printed representation of the string, for Simplify
  - isSameFormula
```
public abstract boolean isSameFormula( Invariant this,
                                      Invariant other)
```
    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.
    
    Parameters:
    
    other - the invariant to compare to this one
    
    Returns:
    
    true iff the two invariants represent the same mathematical formula. Does not consider
    
    Throws:
    
    RuntimeException - if other.getClass() != this.getClass()
  - mergeFormulasOk
```
public boolean mergeFormulasOk( Invariant this)
```
    Returns whether or not it is possible to merge invariants of the same class but with different formulas when combining invariants from lower ppts to build invariants at upper program points. Invariants that have this characteristic (eg, bound, oneof) should override this function. Note that invariants that can do this, normally need special merge code as well (to merge the different formulas into a single formula at the upper point.
    
    Returns:
    
    true if invariants with different formulas can be merged
  - isSameInvariant
```
@Pure
public boolean isSameInvariant( Invariant this,
                               Invariant inv2)
```
    Returns true iff the argument is the "same" invariant as this. Same, in this case, means a matching type, formula, and variable names.
    
    Parameters:
    
    inv2 - the other invariant to compare to this one
    
    Returns:
    
    true iff the argument is the "same" invariant as this
  - isExclusiveFormula
```
@Pure
public boolean isExclusiveFormula( Invariant this,
                                  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. This method does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities.
    
    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 Invariant find(Class<? extends Invariant> invclass,
                                       PptSlice ppt)
```
    Look up a previously instantiated Invariant.
    
    Parameters:
    
    invclass - the class of the invariant to search for
    
    ppt - the program point in which to look for the invariant
    
    Returns:
    
    the invariant of class invclass, or null if none was found
  - get_ni_suppressions
```
@Pure
public @Nullable NISuppressionSet get_ni_suppressions( Invariant this)
```
    Returns the set of non-instantiating suppressions for this invariant. May return null instead of an empty set. Should be overridden by subclasses with non-instantiating suppressions.
    
    Returns:
    
    the set of non-instantiating suppressions for this invariant
  - is_ni_suppressed
```
@EnsuresNonNullIf(result=true,
                  expression="get_ni_suppressions()")
@Pure
public boolean is_ni_suppressed()
```
    Returns whether or not this invariant is ni-suppressed.
    
    Returns:
    
    true if this invariant is ni-suppressed
  - isWorthPrinting
```
@Pure
public boolean isWorthPrinting( Invariant this)
```
  - isObviousStatically
```
@Pure
public final @Nullable DiscardInfo isObviousStatically( Invariant this)
```
    Return true if this invariant is necessarily true from a fact that can be determined statically from the decls files. (An example is being from a certain derivation.) Intended to be overridden by subclasses.
    This method is final because children of Invariant should be extending isObviousStatically(VarInfo[]) because it is more general.
  - isObviousStatically
```
@Pure
public @Nullable DiscardInfo isObviousStatically( Invariant this,
                                                 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. 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
    
    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.
  - isObviousStatically_AllInEquality
```
@Pure
public boolean isObviousStatically_AllInEquality( Invariant this)
```
    Return true if this invariant and all equality combinations of its member variables are necessarily true from a fact that can be determined statically (i.e., the decls files). For example, a == b, and f(a) is obvious, but f(b) is not. In that case, this method on f(a) would return false. If f(b) is also obvious, then this method would return true.
  - isObviousStatically_SomeInEquality
```
@Pure
public @Nullable DiscardInfo isObviousStatically_SomeInEquality( Invariant this)
```
    Return true if this invariant 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.
    
    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.
  - isObviousStatically_SomeInEqualityHelper
```
@Pure
protected @Nullable DiscardInfo isObviousStatically_SomeInEqualityHelper( Invariant this,
                                                                         VarInfo[] vis,
                                                                         VarInfo[] assigned,
                                                                         int position)
```
    Recurse through vis and generate the cartesian product of ...
  - isObvious
```
@Pure
public final @Nullable DiscardInfo isObvious( Invariant this)
```
    Return true if this invariant is necessarily true from a fact that can be determined statically (i.e., the decls files) or dynamically (after checking data). Intended not to be overriden, because sub-classes should override isObviousStatically or isObviousDynamically. Wherever possible, suppression, rather than this, should do the dynamic checking.
  - isObviousDynamically
```
public @Nullable DiscardInfo isObviousDynamically( Invariant this,
                                                  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. 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.
  - isReflexive
```
@Pure
public boolean isReflexive( Invariant this)
```
    Return true if more than one of the variables in the invariant are the same variable. We create such invariants for the purpose of equality set processing, but they aren't intended for printing; there should be invariants with the same meaning but lower arity instead. For instance, we don't need "x = x + x" because we have "x = 0" instead.
    Actually, this isn't strictly true: we don't have an invariant "a[] is a palindrome" corresponding to "a[] is the reverse of a[]", for instance.
  - isObviousDynamically
```
public final @Nullable DiscardInfo isObviousDynamically( Invariant this)
```
    Return true if this invariant is necessarily true from a fact that can be determined dynamically (after checking data, based on other invariants that were inferred). Since this method is dynamic, it should only be called after all processing.
    If a test does not look up other inferred invariants (that is, it relies only on information in the decls file), then it should be written as an isObviousStatically test, not an isObviousDynamically test.
    This method is final because subclasses should extend isObviousDynamically(VarInfo[]) since that method is more general.
  - isObviousDynamically_SomeInEquality
```
@Pure
public @Nullable DiscardInfo isObviousDynamically_SomeInEquality( Invariant this)
```
    Return true if this invariant and 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.
    
    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_SomeInEqualityHelper
```
protected @Nullable DiscardInfo isObviousDynamically_SomeInEqualityHelper( Invariant this,
                                                                          VarInfo[] vis,
                                                                          VarInfo[] assigned,
                                                                          int position)
```
    Recurse through vis (an array of leaders) and generate the cartesian product of their equality sets; in other words, every combination of one element from each equality set. For each such combination, test isObviousDynamically; if any test is true, then return that combination. The combinations are generated via recursive calls to this routine.
  - isAllPrestate
```
@Pure
public boolean isAllPrestate( Invariant this)
```
    Returns true if this invariant is only over prestate variables.
    
    Returns:
    
    true if this invariant is only over prestate variables
  - hasUninterestingConstant
```
public boolean hasUninterestingConstant( Invariant this)
```
    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.
  - match
```
public boolean match(Invariant inv)
```
    Returns whether or not two invariants are of the same type. To be of the same type, invariants must be of the same class. Some invariant classes represent multiple invariants (such as FunctionBinary). They must also be the same formula. Note that invariants with different formulas based on their samples (LinearBinary, Bounds, etc) will still match as long as the mergeFormulaOk() method returns true.
  - state_match
```
public boolean state_match( Invariant this,
                           Object state)
```
    Returns whether or not the invariant matches the specified state. Must be overriden by subclasses that support this. Otherwise, it returns true only if the state is null.
  - createGuardingPredicate
```
public @Nullable Invariant createGuardingPredicate(boolean install)
```
    Create a guarding predicate for a given invariant. Returns null if no guarding is needed.
  - getGuardingList
```
public List<VarInfo> getGuardingList( Invariant this)
```
    Return a list of all the variables that must be non-null in order for this invariant to be evaluated. For instance, it this invariant is "a.b.c > d.e" (where c and e are of integer type), then it doesn't make sense to evaluate the invariant unless "a" is non-null, "a.b" is non-null, and "d" is non-null. So, another way to write the invariant (in "guarded" form) would be "a != null && a.b != null && d != null && a.b.c > d.e".
  - getGuardingList
```
public static List<VarInfo> getGuardingList(VarInfo[] varInfos)
```
    Returns the union of calling VarInfo.getGuardingList on each element of the argument.
    
    Parameters:
    
    varInfos - an array of VarInfo
    
    Returns:
    
    the union of calling VarInfo.getGuardingList on each element of the argument
  - createGuardedInvariant
```
public @Nullable Invariant createGuardedInvariant(boolean install)
```
    This procedure guards one invariant and returns the resulting guarded invariant (implication), without placing it in any slice and without modifying the original invariant. Returns null if the invariant does not need to be guarded.
  - instantiate_dyn
```
protected abstract Invariant instantiate_dyn( Invariant this,
                                             PptSlice slice)
```
    Instantiates (creates) an invariant of the same class on the specified slice. Must be overridden in each class. Must be used rather than clone() so that checks in instantiate(daikon.PptSlice) for reasonable invariants are done.
    The implementation of this method is almost always return new <em>InvName</em>(slice);
    
    Returns:
    
    the new invariant
  - enabled
```
public abstract boolean enabled( Invariant this)
```
    Returns whether or not this class of invariants is currently enabled.
    Its implementation is almost always return dkconfig_enabled;.
  - valid_types
```
public abstract boolean valid_types( Invariant this,
                                    VarInfo[] vis)
```
    Returns whether or not the invariant is valid over the basic types in vis. This only checks basic types (scalar, string, array, etc) and should match the basic superclasses of invariant (SingleFloat, SingleScalarSequence, ThreeScalar, etc). More complex checks that depend on variable details can be implemented in instantiate_ok().
    
    See Also:
    
    instantiate_ok(VarInfo[])
  - instantiate_ok
```
public boolean instantiate_ok( Invariant this,
                              VarInfo[] vis)
```
    Returns true if it makes sense to instantiate this invariant over the specified variables. Checks details beyond what is provided by valid_types(daikon.VarInfo[]). This should never be called without calling valid_types() first (implementations should be able to presume that valid_types() returns true).
    This method does not have to be overridden; the default implementation in Invariant returns true.
    
    See Also:
    
    valid_types(VarInfo[])
  - instantiate
```
public @Nullable Invariant instantiate( Invariant this,
                                       PptSlice slice)
```
    Instantiates this invariant over the specified slice. The slice must not be null and its variables must be valid for this type of invariant. Returns null if the invariant is not enabled or if the invariant is not reasonable over the specified variables. Otherwise returns the new invariant.
  - add_sample
```
public InvariantStatus add_sample( Invariant this,
                                  ValueTuple vt,
                                  int count)
```
    Adds the specified sample to the invariant and returns the result.
    
    Parameters:
    
    vt - the sample to add to this invariant
    
    count - the number of occurrences of the sample to add to this invariant
    
    Returns:
    
    the result of adding the samples to this invariant
  - repCheck
```
public void repCheck( Invariant this)
```
    Check the rep invariants of this.
  - isActive
```
@Pure
public boolean isActive( Invariant this)
```
    Returns whether or not the invariant is currently active. This is used to identify those invariants that require a certain number of points before they actually do computation (eg, LinearBinary)
    This is used during suppresion. Any invariant that is not active cannot suppress another invariant.
    
    Returns:
    
    true if this invariant is currently active
  - logDetail
```
public static boolean logDetail()
```
    Returns true if detailed logging is on. Note that this check is not performed inside the logging calls themselves, it must be performed by the caller.
    
    Returns:
    
    true if detailed logging is on
    
    See Also:
    
    Debug.logDetail(), Debug.logOn(), Debug.log(Logger, Class, Ppt, String)
  - logOn
```
public static boolean logOn()
```
    Returns whether or not logging is on.
    
    See Also:
    
    Debug.logOn()
  - log
```
public void log( Invariant this,
                Logger log,
                String msg)
```
    Logs a description of the invariant and the specified msg via the logger as described in daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String).
    
    Parameters:
    
    log - where to log the message
    
    msg - the message to log
  - log
```
@FormatMethod
public boolean log(@UnknownInitialization(Invariant.class) Invariant this,
                   String format,
                   @Nullable Object... args)
```
    Logs a description of the invariant and the specified msg via the logger as described in daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String).
    
    Parameters:
    
    format - a format string
    
    args - the argumnts to the format string
    
    Returns:
    
    whether or not it logged anything
  - toString
```
@SideEffectFree
public String toString(@GuardSatisfied Invariant this)
```
    Overrides:
    
    toString in class Object
  - toString
```
public static String toString(Invariant[] invs)
```
    Return a string representation of the given invariants.
    
    Parameters:
    
    invs - the invariants to get a string representation of
    
    Returns:
    
    a string representation of the given invariants
  - formatFuzzy
```
public static String formatFuzzy(String method,
                                 VarInfo v1,
                                 VarInfo v2,
                                 OutputFormat format)
```
    Used throughout Java family formatting of invariants.
    Returns
    "plume.FuzzyFloat.method(v1_name, v2_name)"
    Where v1_name and v2_name are the properly formatted varinfos v1 and v2, under the given format.
  - asInvClass
```
public static Class<? extends Invariant> asInvClass(Object x)
```
  - isEqualityComparison
```
public boolean isEqualityComparison()
```
    Returns true if this is an equality comparison. That is, returns true if this Invariant satisfies the following conditions:
    
    the Invariant is an EqualityComparison (its relationship is =, not <, ≤, >, or ≥).
    the invariant is statistically satisfied (its confidence is above the limit)
    This does not consider PairwiseIntComparison to be an equality invariant.
  - checkRep
```
public void checkRep()
```
    Throws an exception if this object is invalid.
    
    Throws:
    
    RuntimeException - if representation invariant on this is broken

Modifier	Constructor	Description
`protected`	`Invariant()`
`protected`	`Invariant(PptSlice ppt)`

Class Invariant

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class Object

Field Detail

debug

debugPrint

debugFlow

debugPrintEquality

debugIsWorthPrinting

debugGuarding

debugIsObvious

dkconfig_confidence_limit

dkconfig_simplify_define_predicates

dkconfig_fuzzy_ratio

invariantEnabledDefault

ppt

falsified

isGuardingPredicate

CONFIDENCE_JUSTIFIED

CONFIDENCE_UNJUSTIFIED

CONFIDENCE_NEVER

PROBABILITY_JUSTIFIED

PROBABILITY_UNJUSTIFIED

PROBABILITY_NEVER

min_mod_non_missing_samples

Constructor Detail

Invariant

Invariant

Method Detail

conf_is_ge

prob_is_ge

confidence_and

confidence_and

confidence_or

prob_and

prob_and

prob_or

enoughSamples

justified

getConfidence

computeConfidence

isExact

falsify

clear_falsified

is_false

clone

transfer

clone_and_permute

resurrect

get_comparability

merge

permute

resurrect_done

usesVar

usesVar

usesVarDerived

varNames

repr

repr_prob

format

format_classname

format_using

isValidEscExpression

isValidExpression

format_unimplemented

format_too_few_samples

simplify_format_double

simplify_format_long

simplify_format_string

isSameFormula

mergeFormulasOk

isSameInvariant

isExclusiveFormula

find

get_ni_suppressions

is_ni_suppressed

isWorthPrinting