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  // We are Serializable, so we specify a version to allow changes to
022  // method signatures without breaking serialization.  If you add or
023  // remove fields, you should change this number to the current date.
024  static final long serialVersionUID = 20040728L;
025
026  // Variables starting with dkconfig_ should only be set via the
027  // daikon.config.Configuration interface.
028  /** Boolean. True iff Positive invariants should be considered. */
029  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
030
031  ///
032  /// Required methods
033  ///
034
035  private Positive(PptSlice ppt) {
036    super(ppt);
037  }
038
039  private @Prototype Positive() {
040    super();
041  }
042
043  private static @Prototype Positive proto = new @Prototype Positive();
044
045  /** Returns the prototype invariant. */
046  public static @Prototype Positive get_proto() {
047    return proto;
048  }
049
050  /** returns whether or not this invariant is enabled */
051  @Override
052  public boolean enabled() {
053    return dkconfig_enabled;
054  }
055
056  /** instantiate an invariant on the specified slice */
057  @Override
058  public Positive instantiate_dyn(@Prototype Positive this, PptSlice slice) {
059    return new Positive(slice);
060  }
061
062  // A printed representation for user output
063  @SideEffectFree
064  @Override
065  public String format_using(@GuardSatisfied Positive this, OutputFormat format) {
066    return var().name() + " > 0";
067  }
068
069  @Override
070  public InvariantStatus check_modified(long v, int count) {
071    if (v <= 0) {
072      return InvariantStatus.FALSIFIED;
073    }
074    return InvariantStatus.NO_CHANGE;
075  }
076
077  @Override
078  public InvariantStatus add_modified(long v, int count) {
079    return check_modified(v, count);
080  }
081
082  @Override
083  protected double computeConfidence() {
084    // Assume that every variable has a .5 chance of being positive by
085    // chance.  Then a set of n values have a have (.5)^n chance of all
086    // being positive by chance.
087    return 1 - Math.pow(.5, ppt.num_samples());
088  }
089
090  @Pure
091  @Override
092  public boolean isSameFormula(Invariant other) {
093    assert other instanceof Positive;
094    return true;
095  }
096}