001package daikon.inv.unary.scalar;
002
003import daikon.PptSlice;
004import daikon.inv.Invariant;
005import daikon.inv.InvariantStatus;
006import daikon.inv.OutputFormat;
007import org.checkerframework.checker.lock.qual.GuardSatisfied;
008import org.checkerframework.dataflow.qual.Pure;
009import org.checkerframework.dataflow.qual.SideEffectFree;
010import typequals.prototype.qual.Prototype;
011
012// This invariant is true if the variable is always positive (greater than 0).
013// This invariant is provided for pedagogical reasons only.
014
015/**
016 * Represents the invariant {@code x > 0} where {@code x} is a long scalar. This exists only as an
017 * example for the purposes of the manual. It isn't actually used (it is replaced by the more
018 * general invariant LowerBound).
019 */
020public class Positive extends SingleScalar {
021  static final long serialVersionUID = 20040728L;
022
023  // Variables starting with dkconfig_ should only be set via the
024  // daikon.config.Configuration interface.
025  /** Boolean. True iff Positive invariants should be considered. */
026  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
027
028  //
029  // Required methods
030  //
031
032  /**
033   * Creates a Positive invariant.
034   *
035   * @param ppt the program point
036   */
037  private Positive(PptSlice ppt) {
038    super(ppt);
039  }
040
041  private @Prototype Positive() {
042    super();
043  }
044
045  private static @Prototype Positive proto = new @Prototype Positive();
046
047  /** Returns the prototype invariant. */
048  public static @Prototype Positive get_proto() {
049    return proto;
050  }
051
052  @Override
053  public boolean enabled() {
054    return dkconfig_enabled;
055  }
056
057  @Override
058  public Positive instantiate_dyn(@Prototype Positive this, PptSlice slice) {
059    return new Positive(slice);
060  }
061
062  @SideEffectFree
063  @Override
064  public String format_using(@GuardSatisfied Positive this, OutputFormat format) {
065    return var().name() + " > 0";
066  }
067
068  @Override
069  public InvariantStatus check_modified(long v, int count) {
070    if (v <= 0) {
071      return InvariantStatus.FALSIFIED;
072    }
073    return InvariantStatus.NO_CHANGE;
074  }
075
076  @Override
077  public InvariantStatus add_modified(long v, int count) {
078    return check_modified(v, count);
079  }
080
081  @Override
082  protected double computeConfidence() {
083    // Assume that every variable has a .5 chance of being positive by
084    // chance.  Then a set of n values have a have (.5)^n chance of all
085    // being positive by chance.
086    return 1 - Math.pow(.5, ppt.num_samples());
087  }
088
089  @Pure
090  @Override
091  public boolean isSameFormula(Invariant other) {
092    assert other instanceof Positive;
093    return true;
094  }
095}