Package daikon.inv.unary.sequence
Class CommonFloatSequence
- Object
-
- Invariant
-
- UnaryInvariant
-
- SingleSequence
-
- SingleFloatSequence
-
- CommonFloatSequence
-
- All Implemented Interfaces:
Serializable
,Cloneable
public class CommonFloatSequence extends SingleFloatSequence
Represents sequences of double values that contain a common subset. Prints as{e1, e2, e3, ...} subset of x[]
.- 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.static boolean
dkconfig_hashcode_seqs
Boolean.-
Fields inherited from class SingleSequence
dkconfig_SeqIndexDisableAll
-
Fields inherited from class Invariant
CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debug, debugFlow, debugGuarding, debugIsObvious, debugIsWorthPrinting, debugPrint, debugPrintEquality, dkconfig_confidence_limit, dkconfig_fuzzy_ratio, dkconfig_simplify_define_predicates, falsified, invariantEnabledDefault, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED
-
-
Constructor Summary
Constructors Modifier Constructor Description protected
CommonFloatSequence()
protected
CommonFloatSequence(PptSlice ppt)
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(double @Interned [] a, int count)
Similar toSingleFloatSequence.check_modified(double[], int)
except that it can change the state of the invariant if necessary.InvariantStatus
check_modified(double @Interned [] a, 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 enabledString
format_csharp_contract()
String
format_daikon()
String
format_using(OutputFormat format)
Return a printed representation of this invariant, in the given format.static CommonFloatSequence
get_proto()
Returns the prototype invariant for CommonFloatSequenceprotected CommonFloatSequence
instantiate_dyn(PptSlice slice)
instantiate an invariant on the specified sliceboolean
instantiate_ok(VarInfo[] vis)
Sequences of hashcode values won't be consistent and are thus not printed by default.boolean
isSameFormula(Invariant other)
Returns true iff the two invariants represent the same mathematical formula.String
repr()
For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob()
also prints the confidence), andInvariant.format()
gives a high-level representation for user output.-
Methods inherited from class SingleFloatSequence
add, add_unmodified, check, check_unmodified, valid_types
-
Methods inherited from class SingleSequence
var
-
Methods inherited from class UnaryInvariant
resurrect_done
-
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, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isExclusiveFormula, isObvious, isObviousDynamically, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, 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
-
-
-
-
Field Detail
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff CommonSequence invariants should be considered.
-
dkconfig_hashcode_seqs
public static boolean dkconfig_hashcode_seqs
Boolean. Set to true to consider common sequences over hashcodes (pointers).
-
-
Constructor Detail
-
CommonFloatSequence
protected CommonFloatSequence(PptSlice ppt)
-
CommonFloatSequence
protected CommonFloatSequence()
-
-
Method Detail
-
get_proto
public static CommonFloatSequence get_proto()
Returns the prototype invariant for CommonFloatSequence
-
enabled
public boolean enabled()
returns whether or not this invariant is enabled
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Sequences of hashcode values won't be consistent and are thus not printed by default.- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
instantiate_dyn
protected CommonFloatSequence instantiate_dyn( CommonFloatSequence this, PptSlice slice)
instantiate an invariant on the specified slice- Specified by:
instantiate_dyn
in classInvariant
- Returns:
- the new invariant
-
repr
public String repr(@GuardSatisfied CommonFloatSequence this)
Description copied from class:Invariant
For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob()
also prints the confidence), andInvariant.format()
gives a high-level representation for user output.
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied CommonFloatSequence this, OutputFormat format)
Description copied from class:Invariant
Return a printed representation of this invariant, in the given format.- Specified by:
format_using
in classInvariant
-
format_daikon
public String format_daikon(@GuardSatisfied CommonFloatSequence this)
-
format_csharp_contract
public String format_csharp_contract(@GuardSatisfied CommonFloatSequence this)
-
check_modified
public InvariantStatus check_modified(double @Interned [] a, int count)
Description copied from class:SingleFloatSequence
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 classSingleFloatSequence
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(double @Interned [] a, int count)
Description copied from class:SingleFloatSequence
Similar toSingleFloatSequence.check_modified(double[], int)
except that it can change the state of the invariant if necessary. If the invariant doesn't have any state, then the implementation should simply callSingleFloatSequence.check_modified(double[], int)
. This method need not check for falsification; that is done by the caller.- Specified by:
add_modified
in classSingleFloatSequence
-
computeConfidence
protected double computeConfidence()
Description copied from class:Invariant
This method computes the confidence that this invariant occurred by chance. Clients should callInvariant.getConfidence()
instead.This method need not check the value of field "falsified", as the caller does that.
- Specified by:
computeConfidence
in classInvariant
- Returns:
- confidence of this invariant
- See Also:
Invariant.getConfidence()
-
isSameFormula
@Pure public boolean isSameFormula(Invariant other)
Description copied from 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.- Specified by:
isSameFormula
in classInvariant
- Parameters:
other
- the invariant to compare to this one- Returns:
- true iff the two invariants represent the same mathematical formula. Does not consider
-
-