Package daikon.inv.binary.sequenceScalar
Class SeqIntLessThan
- Object
-
- Invariant
-
- BinaryInvariant
-
- SequenceScalar
-
- SeqIntLessThan
-
- All Implemented Interfaces:
Serializable
,Cloneable
public final class SeqIntLessThan extends SequenceScalar
Represents an invariant between a long scalar and a a sequence of long values. Prints asx[] elements < y
wherex
is a long sequence andy
is a long scalar.- 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 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, invariantEnabledDefault, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED
-
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(long @Interned [] a, long x, int count)
Similar toSequenceScalar.check_modified(long[], long, int)
except that it can change the state of the invariant if necessary.InvariantStatus
check_modified(long @Interned [] a, long x, int count)
Presents a sample to the invariant.SeqIntLessThan
clone()
Do nothing special, Overridden to remove exception from declaration.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 SeqIntLessThan
find(PptSlice ppt)
String
format_csharp_contract()
String
format_daikon()
String
format_esc()
String
format_java_family(OutputFormat format)
String
format_simplify()
String
format_using(OutputFormat format)
Return a printed representation of this invariant, in the given format.@Nullable NISuppressionSet
get_ni_suppressions()
Returns a list of non-instantiating suppressions for this invariant.static SeqIntLessThan
get_proto()
Returns the prototype invariant for SeqIntLessThanprotected SeqIntLessThan
instantiate_dyn(PptSlice slice)
instantiates the invariant on the specified sliceboolean
instantiate_ok(VarInfo[] vis)
Non-equal SeqIntComparison is only valid on integral types.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
isObviousDynamically(VarInfo[] vis)
Checks to see if this is obvious over the specified variables.@Nullable DiscardInfo
isObviousStatically(VarInfo[] vis)
Checks to see if the comparison is obvious statically.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 SequenceScalar
add, add_unmodified, check, check_unmodified, is_symmetric, resurrect_done, resurrect_done_swapped, resurrect_done_unswapped, 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, checkRep, clear_falsified, 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, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, 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
-
-
-
-
Field Detail
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff SeqIntLessThan invariants should be considered.
-
-
Method Detail
-
get_proto
public static SeqIntLessThan get_proto()
Returns the prototype invariant for SeqIntLessThan
-
enabled
public boolean enabled()
Returns whether or not this invariant is enabled.
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Non-equal SeqIntComparison is only valid on integral types.- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
instantiate_dyn
protected SeqIntLessThan instantiate_dyn( SeqIntLessThan this, PptSlice slice)
instantiates the invariant on the specified slice- Specified by:
instantiate_dyn
in classInvariant
- Returns:
- the new invariant
-
isObviousStatically
@Pure public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis)
Checks to see if the comparison is obvious statically. Makes the following checks:max(A[]) op A[] min(A[]) op A[]
JHP: Note that these are not strict implications, these are merely uninteresting comparisons (except when op is GreaterEqual for max and LessEqual for min).- Overrides:
isObviousStatically
in classInvariant
- 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.
-
clone
@SideEffectFree public SeqIntLessThan clone(@GuardSatisfied SeqIntLessThan this)
Description copied from class:Invariant
Do nothing special, Overridden to remove exception from declaration.
-
repr
public String repr(@GuardSatisfied SeqIntLessThan 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 SeqIntLessThan 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 SeqIntLessThan this)
-
format_esc
public String format_esc(@GuardSatisfied SeqIntLessThan this)
-
format_simplify
public String format_simplify(@GuardSatisfied SeqIntLessThan this)
-
format_java_family
public String format_java_family(@GuardSatisfied SeqIntLessThan this, OutputFormat format)
-
format_csharp_contract
public String format_csharp_contract(@GuardSatisfied SeqIntLessThan this)
-
check_modified
public InvariantStatus check_modified(long @Interned [] a, long x, int count)
Description copied from class:SequenceScalar
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 classSequenceScalar
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 @Interned [] a, long x, int count)
Description copied from class:SequenceScalar
Similar toSequenceScalar.check_modified(long[], long, 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 callSequenceScalar.check_modified(long[], long, int)
. This method need not check for falsification; that is done by the caller.- Specified by:
add_modified
in classSequenceScalar
-
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()
-
isExact
@Pure public boolean isExact()
Description copied from class:Invariant
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.
-
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
-
isExclusiveFormula
@Pure public boolean isExclusiveFormula(Invariant other)
Description copied from class:Invariant
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.- Overrides:
isExclusiveFormula
in classInvariant
- 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 SeqIntLessThan find(PptSlice ppt)
-
isObviousDynamically
@Pure public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis)
Checks to see if this is obvious over the specified variables. Implements the following checks:(x op B[]) ^ (B[] subsequence A[]) ⇒ (x op A[]) (A[] == []) ⇒ (x op A[])
- Overrides:
isObviousDynamically
in classInvariant
-
get_ni_suppressions
@Pure public @Nullable NISuppressionSet get_ni_suppressions()
Returns a list of non-instantiating suppressions for this invariant.- Overrides:
get_ni_suppressions
in classInvariant
- Returns:
- the set of non-instantiating suppressions for this invariant
-
-