Package daikon.inv.binary.twoSequence
Class ReverseFloat
- Object
-
- Invariant
-
- BinaryInvariant
-
- TwoSequenceFloat
-
- ReverseFloat
-
- All Implemented Interfaces:
Serializable
,Cloneable
public class ReverseFloat extends TwoSequenceFloat
Represents two sequences of double where one is in the reverse order of the other. Prints asx[] is the reverse 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 Logger
debug
static boolean
dkconfig_enabled
Boolean.-
Fields inherited from class TwoSequenceFloat
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
ReverseFloat()
protected
ReverseFloat(PptSlice ppt)
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(double @Interned [] a1, double @Interned [] a2, int count)
Default implementation simply calls check.InvariantStatus
check_modified(double @Interned [] a1, double @Interned [] 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 enabledString
format_csharp()
String
format_daikon()
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.static ReverseFloat
get_proto()
Returns the prototype invariant for ReverseFloatReverseFloat
instantiate_dyn(PptSlice slice)
instantiates the invariant on the specified sliceboolean
instantiate_ok(VarInfo[] vis)
Reverse only makes sense on ordered arrays.boolean
isSameFormula(Invariant other)
Return true if both invariants are the same class and the order of the variables (swap) is the same.String
repr()
Returns a representation of the class.protected Invariant
resurrect_done_swapped()
Swaps the variables by inverting the state of swap.-
Methods inherited from class TwoSequenceFloat
add, add_unmodified, check, check_unmodified, get_swap, 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, 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 Reverse invariants should be considered.
-
-
Constructor Detail
-
ReverseFloat
protected ReverseFloat(PptSlice ppt)
-
ReverseFloat
protected ReverseFloat()
-
-
Method Detail
-
get_proto
public static ReverseFloat get_proto()
Returns the prototype invariant for ReverseFloat
-
enabled
public boolean enabled()
returns whether or not this invariant is enabled
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Reverse only makes sense on ordered arrays.- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
instantiate_dyn
public ReverseFloat instantiate_dyn( ReverseFloat this, PptSlice slice)
instantiates the invariant on the specified slice- Specified by:
instantiate_dyn
in classInvariant
- Returns:
- the new invariant
-
resurrect_done_swapped
protected Invariant resurrect_done_swapped()
Description copied from class:TwoSequenceFloat
Swaps the variables by inverting the state of swap.- Overrides:
resurrect_done_swapped
in classTwoSequenceFloat
-
repr
public String repr(@GuardSatisfied ReverseFloat this)
Description copied from class:TwoSequenceFloat
Returns a representation of the class. This includes the classname, variables, and swap state.- Overrides:
repr
in classTwoSequenceFloat
- Returns:
- a string representation of this
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied ReverseFloat 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 ReverseFloat this)
-
format_java_family
public String format_java_family(@GuardSatisfied ReverseFloat this, OutputFormat format)
-
format_csharp
public String format_csharp(@GuardSatisfied ReverseFloat this)
-
format_simplify
public String format_simplify(@GuardSatisfied ReverseFloat this)
-
check_modified
public InvariantStatus check_modified(double @Interned [] a1, double @Interned [] a2, int count)
Description copied from class:TwoSequenceFloat
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 classTwoSequenceFloat
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 [] a1, double @Interned [] a2, int count)
Description copied from class:TwoSequenceFloat
Default implementation simply calls check. Subclasses can override.- Overrides:
add_modified
in classTwoSequenceFloat
-
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.
- Overrides:
computeConfidence
in classTwoSequenceFloat
- Returns:
- confidence of this invariant
- See Also:
Invariant.getConfidence()
-
isSameFormula
@Pure public boolean isSameFormula(Invariant other)
Description copied from class:TwoSequenceFloat
Return true if both invariants are the same class and the order of the variables (swap) is the same.- Overrides:
isSameFormula
in classTwoSequenceFloat
- Parameters:
other
- the invariant to compare to this one- Returns:
- true iff the two invariants represent the same mathematical formula. Does not consider
-
-