Package daikon.inv

Class Implication

    • Field Detail

      • iff

        public boolean iff

    • Method Detail

      • makeImplication

        public static @Nullable Implication makeImplication​(PptTopLevel ppt,
                                                    Invariant predicate,
                                                    Invariant consequent,
                                                    boolean iff,
                                                    Invariant orig_predicate,
                                                    Invariant orig_consequent)
        Creates a new Implication Invariant and adds it to the PptTopLevel.
        Returns:
        null if predicate and the consequent are the same, or if the PptTopLevel already contains this Implication

      • repr

        public String repr​(@GuardSatisfied Implication 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.
        Specified by:
        repr in class Joiner
        Returns:
        a string representation of this

      • 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.

      • 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

      • isObviousStatically_SomeInEquality

        @Pure
public @Nullable DiscardInfo isObviousStatically_SomeInEquality()
        Return true if the right side of the implication and some equality combinations of its member variables are statically obvious. For example, if a == b, and f(a) is obvious, then so is f(b). We use the someInEquality (or least interesting) method during printing so we only print an invariant if all its variables are interesting, since a single, static, non interesting occurance means all the equality combinations aren't interesting.

        This must be overridden for Implication because the right side is the invariant of interest. The standard version passes the vis from the slice containing the implication itself (slice 0).

        Overrides:
        isObviousStatically_SomeInEquality in class Invariant
        Returns:
        the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

      • isObviousDynamically_SomeInEquality

        @Pure
public @Nullable DiscardInfo isObviousDynamically_SomeInEquality()
        Return true if the rightr side of the implication some equality combinations of its member variables are dynamically obvious. For example, a == b, and f(a) is obvious, so is f(b). We use the someInEquality (or least interesting) method during printing so we only print an invariant if all its variables are interesting, since a single, dynamic, non interesting occurance means all the equality combinations aren't interesting.

        This must be overridden for Implication because the right side is the invariant of interest. The standard version passes the vis from the slice containing the implication itself (slice 0).

        Overrides:
        isObviousDynamically_SomeInEquality in class Invariant
        Returns:
        the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

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

      • isSameInvariant

        @EnsuresNonNullIf(result=true,
                  expression="#1")
@Pure
public boolean isSameInvariant​(Invariant other)
        Description copied from class: Invariant
        Returns true iff the argument is the "same" invariant as this. Same, in this case, means a matching type, formula, and variable names.
        Overrides:
        isSameInvariant in class Joiner
        Parameters:
        other - the other invariant to compare to this one
        Returns:
        true iff the argument is the "same" invariant as this

      • hasUninterestingConstant

        public boolean hasUninterestingConstant()
        Description copied from class: Invariant
        An invariant that includes an uninteresting constant (say, "size(x[]) < 237") is likely to be an artifact of the way the program was tested, rather than a statement that would in fact hold over all possible executions.
        Overrides:
        hasUninterestingConstant in class Invariant

      • isAllPrestate

        @Pure
public boolean isAllPrestate()
        Description copied from class: Invariant
        Returns true if this invariant is only over prestate variables.
        Overrides:
        isAllPrestate in class Invariant
        Returns:
        true if this invariant is only over prestate variables

      • log

        public void log​(Logger log,
                String msg)
        Logs a description of the invariant and the specified msg via the logger as described in daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String). Uses the consequent as the logger.
        Overrides:
        log in class Invariant
        Parameters:
        log - where to log the message
        msg - the message to log

      • log

        @FormatMethod
public boolean log​(@UnknownInitialization(Implication.class) Implication this,
                   String format,
                   @Nullable Object... args)
        Logs a description of the invariant and the specified msg via the logger as described in daikon.Debug#log(Logger, Class, Ppt, VarInfo[], String). Uses the consequent as the logger.
        Overrides:
        log in class Invariant
        Parameters:
        format - a format string
        args - the argumnts to the format string
        Returns:
        whether or not it logged anything

      • enabled

        public boolean enabled​( Implication this)
        Description copied from class: Invariant
        Returns whether or not this class of invariants is currently enabled.

        Its implementation is almost always return dkconfig_enabled;.

        Specified by:
        enabled in class Invariant

      • valid_types

        public boolean valid_types​( Implication this,
                           VarInfo[] vis)
        Description copied from class: Invariant
        Returns whether or not the invariant is valid over the basic types in vis. This only checks basic types (scalar, string, array, etc) and should match the basic superclasses of invariant (SingleFloat, SingleScalarSequence, ThreeScalar, etc). More complex checks that depend on variable details can be implemented in instantiate_ok().
        Specified by:
        valid_types in class Invariant
        See Also:
        Invariant.instantiate_ok(VarInfo[])