Problems with the invariant types

18 views
Skip to first unread message

bo yang

unread,
May 20, 2020, 6:52:00 PM5/20/20
to Daikon discuss
Hi all,

I found invariants like "return.items[].getClass().getName() elements == org.jfree.chart.LegendItem.class", but I did not find a counterpart invariant type from the documentation. I guess it belongs to EltOneOfString. But in EltOneOfString, the template is x[] == c (there is no 'elements' before the '==').
EltOneOfString
Represents sequences of String values where the elements of the sequence take on only a few distinct values. Prints as either x[] == c (when there is only one value), or as x[] one of {c1, c2, c3} (when there are multiple values).
See also the following configuration option:

‘daikon.inv.unary.stringsequence.EltOneOfString.size’
 
 BTW, what does the "Elt" mean? Thank you very much!

Regards,
Bo

Michael Ernst

unread,
May 20, 2020, 10:52:30 PM5/20/20
to daikon-discuss
Bo-

Please enable the `daikon.PrintInvariants.print_inv_class` configuration option (described in section "General configuration options", but admittedly hard to find!).  Then Daikon will print the Java class that represents each invariant.  (The invariant looks to me more like it came from EltOneOf than EltOneOfString, but that is just a guess, without access to the inputs that Daikon ran on.)

You are right that the documentation of EltOneOfString (and some other invariants) is incorrect in that it omits the "elements" that is part of the printed representation.  Thank you for pointing that out.  I have fixed it in commit a22a297c.

The `Elt` in the class name means that the invariant is about the elements of the array rather than about the array itself.
Suppose that a variable takes on these values:
 [1, 2, 3]
 [3, 4, 5]
 [1, 2, 3]
 [1, 2, 3]
 [3, 4, 5]
Then an invariant about the array would be that its value is one of { [1, 2, 3], [3, 4, 5] }.
An invariant about the elements would be that the array's elements are one of { 1, 2, 3, 4, 5 }.

Mike

--
You received this message because you are subscribed to the Google Groups "Daikon discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-discus...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/8e0659c4-005a-4541-84e6-5248cf263685%40googlegroups.com.

bo yang

unread,
May 21, 2020, 11:33:21 AM5/21/20
to Daikon discuss
Thank you very much!
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-...@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages