Package daikon.inv.binary.twoSequence

Class PairwiseNumericInt

    • 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 PairwiseNumericInt this)
        Description copied from class: TwoSequence
        Returns a representation of the class. This includes the classname, variables, and swap state.
        Overrides:
        repr in class TwoSequence
        Returns:
        a string representation of this

      • format_using

        @SideEffectFree
public String format_using​(@GuardSatisfied PairwiseNumericInt 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​(long[] x,
                                      long[] y,
                                      int count)
        Calls the function specific equal check and returns the correct status.
        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

      • is_subsequence

        public @Nullable DiscardInfo is_subsequence​(VarInfo[] vis)
        Checks to see if this invariant is over subsequences and if the same relationship holds over the full sequence. This is obvious if it does. For example 'x[foo..] op y[bar..]' would be obvious if 'x[] op y[]' This can't fully be handled as a suppression since a suppression needs to insure that foo == bar as well. But that is not a requirement here (the fact that 'x[] op y[]' implies that foo == bar when x[] and y[] are not missing).

      • 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

      • array_sizes_eq

        public @Nullable InvDef array_sizes_eq​(VarInfo v1,
                                       VarInfo v2)
        Returns an invariant that is true when the size(v1) == size(v2). There are a number of possible cases for an array: 
            x[]         - entire array, size usually available as size(x[])
    x[..(n-1)]  - size is n
    x[..n]      - size is n+1
    x[n..]      - size is size(x[]) - n
    x[(n+1)..]  - size is size(x[]) - (n+1)
        Each combination of the above must be considered in creating the equality invariant. Not all possibilities can be handled. Null is returned in that case. In the following table, s stands for the size 
                            x[]     x[..(n-1)]  x[..n]  x[n..]    x[(n+1)..]
                  --------- ----------  ------  ------    ----------
    y[]           s(y)=s(x)   s(y)=n
    y[..(m-1)]        x         m=n
    y[..m]            x         x         m=n
    y[m..]            x         x          x     m=n ∧
                                                s(y)=s(x)
    y[(m+1)..]        x         x          x        x       m=n ∧
                                                           s(y)=s(x)
        NOTE: this is not currently used. Many (if not all) of the missing table cells above could be filled in with linear binary invariants (eg, m = n + 1).

      • get_array_size

        public @Nullable VarInfo get_array_size​(VarInfo v)
        Returns a variable that corresponds to the size of v. Returns null if no such variable exists. There are two cases that are not handled: x[..n] with an index shift and x[n..].

      • get_format_str

        public abstract String get_format_str​(@GuardSatisfied PairwiseNumericInt 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​(long x,
                                 long 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.