vstolz

3 ms·

1. 1.▲
   by vstolz 12y ago

   It is possible, see e.g. http://ssrg.nicta.com.au/projects/TS/ , though it's not really the tutorial you've been hoping for.
2. 2.▲
   by vstolz 12y ago

   With tools like Coq, you may even have the benefit of extracting an implementation from your proof! Some assembly may be required though, and extraction only works to functional languages.
3. 3.▲
   by vstolz 12y ago

   Sorry to keep following up, but we'd really like to know what we can improve -- into which tool? Are you talking about the KeY tool, or the various libraries they are now catching up on this issue?
4. 4.▲
   by vstolz 12y ago

   What are you looking for?
5. 5.▲
   by vstolz 12y ago

   There is also http://bugs.java.com/view_bug.do?bug_id=8011944 , where IIUC the suggested "fix" was to use a VM switch to enable the old (and slower) sorting...
6. 6.▲
   by vstolz 12y ago

   I'd say that QuickCheck would have a hard time coming up with a failing test case since the input needs to be rather large to trigger the bug.