Package daikon.tools.runtimechecker

Class Property

    • Field Detail

      • jmlRep

        public String jmlRep
        JML representation of this property.

      • confidence

        public double confidence
        A measure of a property's universality: whether it captures the general behavior of the program. The measure ranges from 0 (no confidence) to 1 (high confidence).

      • daikonClass

        public String daikonClass
        The Daikon class name that this property represents.

    • Method Detail

      • method

        public String method​(@GuardSatisfied Property this)
        The name of the method that this property describes. ("null" for object invariants.)

      • kind

        public Property.Kind kind​(@GuardSatisfied Property this)
        The kind of property (enter, exit or objectInvariant).

      • daikonRep

        public String daikonRep​(@GuardSatisfied Property this)
        Daikon representation (as output by Daikon's default output format).

      • toString

        @SideEffectFree
public String toString​(@GuardSatisfied Property this)
        Easy-on-the-eye string representation.
        Overrides:
        toString in class Object

      • equals

        @EnsuresNonNullIf(result=true,
                  expression="#1")
@Pure
public boolean equals​(@GuardSatisfied Property this,
                      @GuardSatisfied @Nullable Object o)
        Two properties are equal if their fields daikonRep, method and kind are equal. The other fields may differ.
        Overrides:
        equals in class Object

      • hashCode

        @Pure
public int hashCode​(@GuardSatisfied @UnknownSignedness Property this)
        Overrides:
        hashCode in class Object

      • get

        public static Property get​(String annoString)
                    throws MalformedPropertyException
        Parse a String and return the property that it represents. An example of the String representation of an property is: 
        
 <INVINFO>
 <INV> this.topOfStack <= this.theArray.length-1 </INV>
 <ENTER>
 <DAIKON>  this.topOfStack <= size(this.theArray[])-1  </DAIKON>
 <DAIKONCLASS>class daikon.inv.binary.twoScalar.IntLessEqual</DAIKONCLASS>
 <METHOD>  isEmpty()  </METHOD>
 </INVINFO>

        The above string should actually span only one line.

        To be well-formed, a property should be enclosed in <INVINFO> tags, contain <DAIKON> and <METHOD> tags, and exactly one of <ENTER>, <EXIT>, <OBJECT>, or <CLASS>.

        Throws:
        MalformedPropertyException

      • xmlString

        public String xmlString()
        XML representation. May be diferent from the String used to parse the property; only those tags that were parsed by the get() method will be output here.

      • xmlStringNoJml

        public String xmlStringNoJml()
        Similar to xmlString(), but without a <INV>...</INV> tag (the JML representation).

        Invariant: this.equals(Property.get(this.xmlStringNoJml())

      • findProperties

        public static Property[] findProperties​(String annoString)
        Find, parse and return all well-formed XML String representing properties. String. The string annoString may contain none, one, or several properties. Ignores malformed properties.

      • findProperties

        public static Property[] findProperties​(List<String> annoStrings)
        Find, parse and return all distinct properties found in a list of strings. Each string in annoStrings may contain none, one, or several properties. Malformed properties are ignored.

      • calculateConfidence

        public double calculateConfidence()
        A heuristic technique that takes into account several factors when calculating the confidence of an property, among them:
        • The values of property.kind().
        • The "Daikon class" of the property.
        • Whether the property relates old and new state.
        • The total number of properties in the method containing this property.

      • maxConf

        public static double maxConf​(Property[] annos)
        The maximum confidence value calculated among all Properties given.

      • confidence

        public static double confidence​(Property[] annos)
        The confidence of a set of properties. Currently it's just the maximum confidence.