3 ms·
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
- kjeetgill 8y agoHuh, interesting that they picked OpenJDK 6 for this work. Any clue why?
- slaymaker1907 8y agoI suspect that it is because Java 6 is the oldest (and thus smallest/simplest) version of Java that supports their tooling. Java 6 introduced annotations which makes writing third party tooling a lot easier plus Java 7 changed the sort algorithm. This particular update which used Timsort actually had some subtle issues which were only found through formal verification [1]. Not sure if there were other changes to collections internally/externally though. [1]: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...