public abstract class Invariant extends Object implements Serializable, Cloneable
Modifier and Type  Class and 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)
Note that this is based on the Invariant type (i.e., class) and the
internal state and not on what ppt the invariant is in or what
variables it is over.

Modifier and Type  Field and 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
Floatingpoint number between 0 and 1.

static double 
dkconfig_fuzzy_ratio
Floatingpoint 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.

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 
Modifier  Constructor and Description 

protected 
Invariant() 
protected 
Invariant(PptSlice ppt) 
Modifier and Type  Method and 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 
clear_falsified()
Clear the falsified flag.

Invariant 
clone_and_permute(int[] permutation)
Clones the invariant and then permutes it as specified.

Invariant 
clone()
Do nothing special, Overridden to remove
exception from declaration

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 confidence that both conditions are satisfied.

static double 
confidence_and(double c1,
double c2,
double c3)
Return the confidence that all three conditions are satisfied.

static double 
confidence_or(double c1,
double c2)
Return the confidence that either condition is satisfied.

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.

Invariant 
createGuardingPredicate(boolean install)
Create a guarding predicate for a given invariant.

boolean 
enabled()
Returns whether or not this class of invariants are currently
enabled

boolean 
enoughSamples() 
void 
falsify()
Marks the invariant as falsified.

static Invariant 
find(Class<? extends Invariant> invclass,
PptSlice ppt)
Look up a previously instantiated Invariant.

String 
format_too_few_samples(OutputFormat request,
String attempt) 
String 
format_unimplemented(OutputFormat request) 
abstract String 
format_using(OutputFormat format) 
String 
format()
For printing invariants, there are two interfaces:
repr gives a lowlevel representation
(repr_prop also prints the confidence), and
format gives a highlevel representation for user output.

static String 
formatFuzzy(String method,
VarInfo v1,
VarInfo v2,
OutputFormat format)
Used throught Java family formatting of invariants.

VarComparability 
get_comparability()
Returns a single VarComparability that describes the set of
variables used by this invariant.

NISuppressionSet 
get_ni_suppressions()
Returns the set of noninstantiating 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 nonnull 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()
This is the test that's planned to replace the poorly specified
"isInteresting" check.

protected Invariant 
instantiate_dyn(PptSlice slice)
Instantiates an invariant of the same class on the specified
slice.

boolean 
instantiate_ok(VarInfo[] vis)
Checks to see if the invariant can reasonably be instantiated over
the specified variables.

Invariant 
instantiate(PptSlice slice)
Instantiates this invariant over the specified slice.

boolean 
is_false()
Returns whether or not this invariant has been destroyed.

boolean 
is_ni_suppressed()
Returns whether or not this invariant is nisuppressed.

boolean 
isActive()
Returns whether or not the invariant is currently active.

boolean 
isAllPrestate() 
boolean 
isExact()
Subclasses should override.

boolean 
isExclusiveFormula(Invariant other) 
boolean 
isInteresting() 
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).

DiscardInfo 
isObviousDynamically_SomeInEquality()
Return true if this invariant and some equality combinations of
its member variables are dynamically obvious.

protected 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.

DiscardInfo 
isObviousDynamically()
Return true if this invariant is necessarily true from a fact
that can be determined dynamically (after checking data).

DiscardInfo 
isObviousDynamically(VarInfo[] vis)
Return nonnull 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.

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

DiscardInfo 
isObviousStatically_SomeInEquality()
Return true if this invariant and some equality combinations of
its member variables are statically obvious.

protected DiscardInfo 
isObviousStatically_SomeInEqualityHelper(VarInfo[] vis,
VarInfo[] assigned,
int position)
Recurse through vis and generate the cartesian product of ...

DiscardInfo 
isObviousStatically()
Return true if this invariant is necessarily true from a fact
that can be determined statically (i.e., the decls files) (e.g.,
by being from a certain derivation).

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 
isReflexive()
Return true if more than one of the variables in the invariant
are the same variable.

boolean 
isSameFormula(Invariant other) 
boolean 
isSameInvariant(Invariant inv2) 
boolean 
isValidEscExpression() 
boolean 
isValidExpression(OutputFormat format) 
boolean 
isWorthPrinting() 
boolean 
justified()
A wrapper around getConfidence() or getConfidence().

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 format,
Object... args)
Logs a description of the invariant and the specified msg via the
logger as described in
Debug.log(Logger, Class, Ppt,
VarInfo[], String) . 
static boolean 
logDetail()
Returns whether or not 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.

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 probability that both conditions are satisfied.

static double 
prob_and(double p1,
double p2,
double p3)
Return the probability that all three conditions are satisfied.

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 probability that either condition is satisfied.

void 
repCheck()
Check the rep invariants of this.

String 
repr_prob()
For printing invariants, there are two interfaces:
repr gives a lowlevel representation
(repr_prop also prints the confidence), and
format gives a highlevel representation for user output.

String 
repr()
For printing invariants, there are two interfaces:
repr gives a lowlevel representation
(repr_prop also prints the confidence), and
format gives a highlevel representation for user output.

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.

Invariant 
resurrect(PptSlice new_ppt,
int[] permutation)
Take a falsified invariant and resurrect it in a new PptSlice.

static String 
simplify_format_double(double d)
Convert a floating point value into the weird Modula3like
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) 
Invariant 
transfer(PptSlice new_ppt,
int[] permutation)
Take an invariant and transfer it into a new PptSlice.

boolean 
usesVar(String name) 
boolean 
usesVar(VarInfo vi) 
boolean 
usesVarDerived(String name) 
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.

public static final Logger debugPrint
public static final Logger debugPrintEquality
public static final Logger debugIsWorthPrinting
public static final Logger debugGuarding
public static final Logger debugIsObvious
public static double dkconfig_confidence_limit
public static boolean dkconfig_simplify_define_predicates
public static double dkconfig_fuzzy_ratio
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.public PptSlice ppt
protected boolean falsified
public boolean isGuardingPredicate
public static final double CONFIDENCE_JUSTIFIED
public static final double CONFIDENCE_UNJUSTIFIED
public static final double CONFIDENCE_NEVER
public static final double PROBABILITY_JUSTIFIED
public static final double PROBABILITY_UNJUSTIFIED
public static final double PROBABILITY_NEVER
public static final int min_mod_non_missing_samples
public static final double conf_is_ge(double x, double goal)
public static final double prob_is_ge(double x, double goal)
public static final double confidence_and(double c1, double c2)
public static final double confidence_and(double c1, double c2, double c3)
public static final double confidence_or(double c1, double c2)
public static final double prob_and(double p1, double p2)
public static final double prob_and(double p1, double p2, double p3)
public static final double prob_or(double p1, double p2)
public boolean enoughSamples()
public final boolean justified()
public final double getConfidence()
As an example, if the invariant is "x!=0", and 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 need not check the value of field "falsified", as the caller does that.
This method is a wrapper around computeConfidence(), which does the actual work.
computeConfidence()
protected abstract double computeConfidence()
getConfidence()
public boolean isExact()
public void falsify()
public void clear_falsified()
public boolean is_false()
public Invariant transfer(PptSlice new_ppt, int[] permutation)
new_ppt
 must have the same arity and typespermutation
 gives the varinfo array index mapping in the
new pptpublic Invariant clone_and_permute(int[] permutation)
public Invariant resurrect(PptSlice new_ppt, int[] permutation)
new_ppt
 must have the same arity and typespermutation
 gives the varinfo array index mappingpublic VarComparability get_comparability()
public Invariant merge(List<Invariant> invs, PptSlice parent_ppt)
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 invariantpublic Invariant permute(int[] permutation)
protected abstract Invariant resurrect_done(int[] permutation)
public boolean usesVarDerived(String name)
public String repr()
public String repr_prob()
public String format()
public abstract String format_using(OutputFormat format)
public boolean isValidEscExpression()
VarInfo.isValidEscExpression()
public boolean isValidExpression(OutputFormat format)
public String format_unimplemented(OutputFormat request)
public String format_too_few_samples(OutputFormat request, String attempt)
public static String simplify_format_double(double d)
public static String simplify_format_long(long l)
public static String simplify_format_string(String s)
public boolean isSameFormula(Invariant other)
RuntimeException
 if other.getClass() != this.getClass()public boolean mergeFormulasOk()
public boolean isSameInvariant(Invariant inv2)
public boolean isExclusiveFormula(Invariant other)
public static Invariant find(Class<? extends Invariant> invclass, PptSlice ppt)
public NISuppressionSet get_ni_suppressions()
public boolean is_ni_suppressed()
public boolean isWorthPrinting()
public final DiscardInfo isObviousStatically()
This method is final because children of Invariant should be extending isObviousStatically(VarInfo[]) because it is more general.
public DiscardInfo isObviousStatically(VarInfo[] vis)
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.public boolean isObviousStatically_AllInEquality()
public DiscardInfo isObviousStatically_SomeInEquality()
protected DiscardInfo isObviousStatically_SomeInEqualityHelper(VarInfo[] vis, VarInfo[] assigned, int position)
public final DiscardInfo isObvious()
public DiscardInfo isObviousDynamically(VarInfo[] vis)
public boolean isReflexive()
public final DiscardInfo isObviousDynamically()
This method is final because subclasses should extend isObviousDynamically(VarInfo[]) since that method is more general.
public DiscardInfo isObviousDynamically_SomeInEquality()
protected DiscardInfo isObviousDynamically_SomeInEqualityHelper(VarInfo[] vis, VarInfo[] assigned, int position)
public boolean isAllPrestate()
public boolean isInteresting()
public boolean hasUninterestingConstant()
public boolean match(Invariant inv)
public boolean state_match(Object state)
public Invariant createGuardingPredicate(boolean install)
public List<VarInfo> getGuardingList()
public static List<VarInfo> getGuardingList(VarInfo[] varInfos)
public Invariant createGuardedInvariant(boolean install)
protected Invariant instantiate_dyn(PptSlice slice)
public boolean enabled()
public boolean valid_types(VarInfo[] vis)
instantiate_ok(VarInfo[])
public boolean instantiate_ok(VarInfo[] vis)
valid_types(VarInfo[])
public Invariant instantiate(PptSlice slice)
public InvariantStatus add_sample(ValueTuple vt, int count)
public void repCheck()
public boolean isActive()
public static boolean logDetail()
public static boolean logOn()
Debug.logOn()
public void log(Logger log, String msg)
Debug.log(Logger, Class, Ppt,
VarInfo[], String)
.public boolean log(String format, Object... args)
Debug.log(Logger, Class, Ppt,
VarInfo[], String)
.public static String formatFuzzy(String method, VarInfo v1, VarInfo v2, OutputFormat format)
public static Class<? extends Invariant> asInvClass(Object x)