Package daikon.inv.binary.twoSequence

Class SuperSequence

Object

Invariant

BinaryInvariant

TwoSequence

SuperSequence

All Implemented Interfaces:

Serializable, Cloneable

public class SuperSequence
extends TwoSequence

Represents two sequences of long values where one sequence is a subsequence of the other. Prints as x[] is a subsequence of y[].

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

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

Field Summary

Fields

Modifier and Type	Field	Description
static boolean	dkconfig_enabled	Boolean.

Fields inherited from class TwoSequence

swap

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, invariantEnabledDefault, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	SuperSequence()
protected	SuperSequence(PptSlice ppt)

Method Summary

Modifier and Type	Method	Description
InvariantStatus	add_modified(long[] a1, long[] a2, int count)	Default implementation simply calls check.
InvariantStatus	check_modified(long[] a1, long[] a2, int count)	Presents a sample to the invariant.
protected double	computeConfidence()	This method computes the confidence that this invariant occurred by chance.
boolean	enabled()	returns whether or not this invariant is enabled
static @Nullable SuperSequence	find(PptSlice ppt)
String	format_csharp_contract()
String	format_daikon()
String	format_simplify()
String	format_using(OutputFormat format)	Return a printed representation of this invariant, in the given format.
NISuppressionSet	get_ni_suppressions()	returns the ni-suppressions for SubSequence
static SuperSequence	get_proto()	Returns the prototype invariant for SuperSequence
protected SuperSequence	instantiate_dyn(PptSlice slice)	instantiates the invariant on the specified slice
@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	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.
static @Nullable DiscardInfo	isObviousSubSequence(Invariant inv, VarInfo subvar, VarInfo supervar)	Returns a DiscardInfo, or null if the Invariant is not an obvious subsequence.
static @Nullable IPair<DiscardCode,String>	isObviousSubSequence(VarInfo subvar, VarInfo supervar)	Returns a IPair of a DiscardCode and a discardReason string, or null if the Invariant is not an obvious subsequence.
static boolean	isObviousSubSequenceDynamically(Invariant inv, VarInfo subvar, VarInfo supervar)	Returns true if the two original variables are related in a way that makes subsequence or subset detection not informative.
boolean	isSameFormula(Invariant inv)	Return true if both invariants are the same class and the order of the variables (swap) is the same.
protected Invariant	resurrect_done_swapped()	Swaps the variables by inverting the state of swap.

Methods inherited from class TwoSequence

add, add_unmodified, check, check_unmodified, get_swap, repr, resurrect_done, resurrect_done_unswapped, valid_types, var1, var1, var2, var2

Methods inherited from class BinaryInvariant

add_unordered, check_unordered, find, is_symmetric

Methods inherited from class Invariant

add_sample, asInvClass, checkRep, clear_falsified, clone, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, instantiate_ok, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isExclusiveFormula, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, 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

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff SubSequence invariants should be considered.

Constructor Detail

SuperSequence

protected SuperSequence(PptSlice ppt)

SuperSequence

protected SuperSequence()

Method Detail

get_proto

public static SuperSequence get_proto()

Returns the prototype invariant for SuperSequence

enabled

public boolean enabled()

returns whether or not this invariant is enabled

Specified by:

enabled in class Invariant

instantiate_dyn

protected SuperSequence instantiate_dyn( SuperSequence this,
                                        PptSlice slice)

instantiates the invariant on the specified slice

Specified by:

instantiate_dyn in class Invariant

Returns:

the new invariant

resurrect_done_swapped

protected Invariant resurrect_done_swapped()

Description copied from class: TwoSequence

Swaps the variables by inverting the state of swap.

Overrides:

resurrect_done_swapped in class TwoSequence

format_using

@SideEffectFree
public String format_using(@GuardSatisfied SuperSequence this,
                           OutputFormat format)

Description copied from class: Invariant

Return a printed representation of this invariant, in the given format.

Specified by:

format_using in class Invariant

format_daikon

public String format_daikon(@GuardSatisfied SuperSequence this)

format_csharp_contract

public String format_csharp_contract(@GuardSatisfied SuperSequence this)

format_simplify

public String format_simplify(@GuardSatisfied SuperSequence this)

check_modified

public InvariantStatus check_modified(long[] a1,
                                      long[] a2,
                                      int count)

Description copied from class: TwoSequence

Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.

Specified by:

check_modified in class TwoSequence

count - how many identical samples were observed in a row. For example, three calls to check_modified with a count parameter of 1 is equivalent to one call to check_modified with a count parameter of 3.

Returns:

whether or not the sample is consistent with the invariant

add_modified

public InvariantStatus add_modified(long[] a1,
                                    long[] a2,
                                    int count)

Description copied from class: TwoSequence

Default implementation simply calls check. Subclasses can override.

Overrides:

add_modified in class TwoSequence

computeConfidence

protected double computeConfidence()

Description copied from class: Invariant

This method computes the confidence that this invariant occurred by chance. Clients should call Invariant.getConfidence() instead.

This method need not check the value of field "falsified", as the caller does that.

Overrides:

computeConfidence in class TwoSequence

Returns:

confidence of this invariant

See Also:

Invariant.getConfidence()

isObviousSubSequence

@Pure
public static @Nullable DiscardInfo isObviousSubSequence(Invariant inv,
                                                         VarInfo subvar,
                                                         VarInfo supervar)

Returns a DiscardInfo, or null if the Invariant is not an obvious subsequence.

Returns:

a DiscardInfo, or null if the Invariant is not an obvious subsequence

isObviousSubSequence

@Pure
public static @Nullable IPair<DiscardCode,String> isObviousSubSequence(VarInfo subvar,
                                                                             VarInfo supervar)

Returns a IPair of a DiscardCode and a discardReason string, or null if the Invariant is not an obvious subsequence.

Returns:

a IPair of a DiscardCode and a discardReason string, or null if the Invariant is not an obvious subsequence

find

public static @Nullable SuperSequence find(PptSlice ppt)

isObviousStatically

@Pure
public @Nullable 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

@Pure
public @Nullable 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

isObviousSubSequenceDynamically

public static boolean isObviousSubSequenceDynamically(Invariant inv,
                                                      VarInfo subvar,
                                                      VarInfo supervar)

Returns true if the two original variables are related in a way that makes subsequence or subset detection not informative.

isSameFormula

@Pure
public boolean isSameFormula(Invariant inv)

Description copied from class: TwoSequence

Return true if both invariants are the same class and the order of the variables (swap) is the same.

Overrides:

isSameFormula in class TwoSequence

Parameters:

inv - the invariant to compare to this one

Returns:

true iff the two invariants represent the same mathematical formula. Does not consider

get_ni_suppressions

@Pure
public NISuppressionSet get_ni_suppressions()

returns the ni-suppressions for SubSequence

Overrides:

get_ni_suppressions in class Invariant

Returns:

the set of non-instantiating suppressions for this invariant