xiaohe27
commented
8 years ago Some time ago, I proposed a modification to a similar property called SortedSet_Comparable which only reports violation when it neither implements Comparable nor uses comparator:
https://github.com/runtimeverification/property-db/commit/b065be011c660062654f400184206e8352899ca6
The monitor should still be able to report the 'true' bug no matter whether JVM will throw Exception, so I think we'd better keep this property.
@owolabileg what do you think?
The property TreeSet_Comparable (https://goo.gl/3cxBUf) requires the object to be put into a TreeSet/SortedSet instance to implement Comparable interface. According to Java 6 specification (https://goo.gl/n91l2v), to put an object into a typed TreeSet, either the type class itself implements Comparable or the TreeSet is constructed with a user-defined Comparator that takes the type class. If none of the above 2 requirements is satisified, JVM will throw an Exception. When this property is triggered with successful running, it can only be false alarms against programs using comparators for TreeSet construction, which are legal under Java API specification. We'd suggest to remove this property as it could only trigger false alarms without providing information for eliminating true bugs beside what has been provided by the Exception on JVM.