daikon.inv.binary.sequenceScalar
Class Member

Object
  Invariant
      BinaryInvariant
          SequenceScalar
              Member

All Implemented Interfaces:

Serializable, Cloneable

public final class Member
extends SequenceScalar

Represents long scalars that are always members of a sequence of long values. Prints as x in y[] where x is a long scalar and y[] is a sequence of long.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

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

Field Summary

static Logger	debug
static boolean	dkconfig_enabled Boolean.

Fields inherited from class Invariant

CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, 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	Member()
protected	Member(PptSlice ppt)

Method Summary

InvariantStatus	add_modified(long[] a, long i, int count) This method need not check for falsified; that is done by the caller.
InvariantStatus	check_modified(long[] a, long i, int count)
protected double	computeConfidence() This method computes the confidence that this invariant occurred by chance.
boolean	enabled() Returns whether or not this invariant is enabled
String	format_daikon()
String	format_esc()
String	format_java_family(OutputFormat format)
String	format_java()
String	format_simplify()
String	format_using(OutputFormat format)
static Member	get_proto() Returns the prototype invariant for Member
protected Member	instantiate_dyn(PptSlice slice) instantiates the invariant on the specified slice
DiscardInfo	isObviousDynamically(VarInfo[] vis) Checks to see if this is obvious over the specified variables.
static boolean	isObviousMember(VarInfo sclvar, VarInfo seqvar) Check whether sclvar is a member of seqvar can be determined statically.
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)
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 SequenceScalar

add_unmodified, add, check_unmodified, check, is_symmetric, resurrect_done_swapped, resurrect_done_unswapped, resurrect_done, scl_index, sclvar, sclvar, seq_first, seq_index, seqvar, seqvar, valid_types

Methods inherited from class BinaryInvariant

add_unordered, check_unordered, find, get_swap

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, enoughSamples, falsify, find, format_too_few_samples, format_unimplemented, format, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate_ok, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isExact, isExclusiveFormula, isInteresting, isObvious, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousDynamically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isObviousStatically, isReflexive, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, 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, varNames

Methods inherited from class Object

equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

debug

public static final Logger debug

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff Member invariants should be considered.

Constructor Detail

Member

protected Member(PptSlice ppt)

Member

protected Member()

Method Detail

get_proto

public static Member get_proto()

Returns the prototype invariant for Member

enabled

public boolean enabled()

Returns whether or not this invariant is enabled

Overrides:

enabled in class Invariant

instantiate_dyn

protected Member instantiate_dyn(PptSlice slice)

instantiates the invariant on the specified slice

Overrides:

instantiate_dyn in class Invariant

Returns:

the new invariant

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.

isObviousMember

public static boolean isObviousMember(VarInfo sclvar,
                                      VarInfo seqvar)

Check whether sclvar is a member of seqvar can be determined statically.

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.

Overrides:

repr in class Invariant

format_using

public String format_using(OutputFormat format)

Specified by:

format_using in class Invariant

format_daikon

public String format_daikon()

format_java

public String format_java()

format_java_family

public String format_java_family(OutputFormat format)

format_esc

public String format_esc()

format_simplify

public String format_simplify()

check_modified

public InvariantStatus check_modified(long[] a,
                                      long i,
                                      int count)

Specified by:

check_modified in class SequenceScalar

add_modified

public InvariantStatus add_modified(long[] a,
                                    long i,
                                    int count)

Description copied from class: SequenceScalar

This method need not check for falsified; that is done by the caller.

Specified by:

add_modified in class SequenceScalar

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

isSameFormula

public boolean isSameFormula(Invariant other)

Overrides:

isSameFormula in class Invariant

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.

isObviousDynamically

public DiscardInfo isObviousDynamically(VarInfo[] vis)

Checks to see if this is obvious over the specified variables. Implements the following checks:

   (0 <= i <= j) ^ (A[] == B[]) ==> A[i] in B[0..j]
   (0 <= i <= j) ^ (A[] == B[]) ==> A[j] in B[i..]
   (A subset B)                 ==> A[i] in B
 

Overrides:

isObviousDynamically in class Invariant