Package daikon.inv.binary.sequenceScalar

Class Member

  • All Implemented Interfaces:
    Serializable, Cloneable
    public final class Member
extends SequenceScalar
    Represents long scalars that are always members of a sequence of long values. Prints as x in y[] where x is a long scalar and y[] is a sequence of long.
    See Also:
    Serialized Form

    • Field Detail

      • dkconfig_enabled

        public static boolean dkconfig_enabled
        Boolean. True iff Member invariants should be considered.

    • Method Detail

      • get_proto

        public static Member get_proto()
        Returns the prototype invariant for Member

      • enabled

        public boolean enabled()
        Returns whether or not this invariant is enabled.
        Specified by:
        enabled in class Invariant

      • isObviousStatically

        @Pure
public @Nullable DiscardInfo isObviousStatically​(VarInfo[] vis)
        Description copied from class: Invariant
        Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this. Conceptually, this means "is this invariant statically obvious if its VarInfos were switched with vis?" Intended to be overridden by subclasses. Should only do static checking.

        Precondition: vis.length == this.ppt.var_infos.length

        Overrides:
        isObviousStatically in class Invariant
        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.

      • isObviousMember

        @Pure
public static boolean isObviousMember​(VarInfo sclvar,
                                      VarInfo seqvar)
        Check whether sclvar is a member of seqvar can be determined statically.

      • repr

        public String repr​(@GuardSatisfied Member 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), and Invariant.format() gives a high-level representation for user output.
        Overrides:
        repr in class Invariant
        Returns:
        a string representation of this

      • check_modified

        public InvariantStatus check_modified​(long @Interned [] a,
                                      long i,
                                      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 class SequenceScalar
        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

      • 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 class Invariant
        Parameters:
        other - the invariant to compare to this one
        Returns:
        true iff the two invariants represent the same mathematical formula. Does not consider

      • isObviousDynamically

        @Pure
public @Nullable DiscardInfo isObviousDynamically​(VarInfo[] vis)
        Checks to see if this is obvious over the specified variables. Implements the following checks: 
           (0 ≤ i ≤ j) ^ (A[] == B[]) ⇒ A[i] in B[0..j]
   (0 ≤ i ≤ j) ^ (A[] == B[]) ⇒ A[j] in B[i..]
   (A subset B)                       ⇒ A[i] in B
        Overrides:
        isObviousDynamically in class Invariant