Class Positive

  • All Implemented Interfaces:
    Serializable, Cloneable

    public class Positive
    extends SingleScalar
    Represents the invariant x > 0 where x is a long scalar. This exists only as an example for the purposes of the manual. It isn't actually used (it is replaced by the more general invariant LowerBound).
    See Also:
    Serialized Form
    • Field Detail

      • dkconfig_enabled

        public static boolean dkconfig_enabled
        Boolean. True iff Positive invariants should be considered.
    • Method Detail

      • enabled

        public boolean enabled()
        returns whether or not this invariant is enabled
        Specified by:
        enabled in class Invariant
      • check_modified

        public InvariantStatus check_modified​(long v,
                                              int count)
        Description copied from class: SingleScalar
        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 SingleScalar
        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