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}