Package daikon.inv.binary.twoScalar

Class NumericFloat

    • Method Detail

      • 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.
        Overrides:
        isExact in class Invariant
        Returns:
        true if any variable value can be computed from all the others

      • repr

        public String repr​(@GuardSatisfied NumericFloat this)
        Description copied from class: TwoFloat
        Returns a representation of the class. This includes the classname, variables, and swap state.
        Overrides:
        repr in class TwoFloat
        Returns:
        a string representation of this

      • format_using

        @SideEffectFree
public String format_using​(@GuardSatisfied NumericFloat this,
                           OutputFormat format)
        Returns a string in the specified format that describes the invariant. The generic format string is obtained from the subclass specific get_format_str(). Instances of %varN% are replaced by the variable name in the specified format.
        Specified by:
        format_using in class Invariant

      • check_modified

        public InvariantStatus check_modified​(double x,
                                      double y,
                                      int count)
        Calls the function specific equal check and returns the correct status.
        Specified by:
        check_modified in class TwoFloat
        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

      • is_subscript

        public @Nullable DiscardInfo is_subscript​(VarInfo[] vis)
        Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'. Doesn't catch the case where a = b+1.

      • 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

      • get_format_str

        public abstract String get_format_str​(@GuardSatisfied NumericFloat this,
                                      OutputFormat format)
        Return a format string for the specified output format. Each instance of %varN% will be replaced by the correct name for varN.

      • eq_check

        public abstract boolean eq_check​(double x,
                                 double y)
        Returns true if x and y don't invalidate the invariant.

      • obvious_checks

        public InvDef[][] obvious_checks​(VarInfo[] vis)
        Returns an array of arrays of antecedents. If all of the antecedents in any array are true, then the invariant is obvious.