OpenJML / OpenJML

This is the primary repository for the source code of the OpenJML project. The source code is licensed under GPLv2 because it derives from OpenJDK which is so licensed. The active issues list for OpenJML development is here and the wiki contains information relevant to development. Public documentation for users is at the project website:
http://www.openjml.org
141 stars 33 forks source link

A Large Set of Examples (Available) #800

Closed marcel139 closed 1 year ago

marcel139 commented 1 year ago

In the following link, I provide a large set of examples:

https://www.dropbox.com/s/yvddtb7inh1v2y2/JML.zip?dl=0

They are originally from the OpenJML tutorial (thanks @davidcok) and @leavens 2007 tutorial:

Two important considerations:

  1. The file tutorial/exercises/Cap_02_3_Assert_Q2_s.java is not working; its verification causes the Error Message: "Solver has unexpectedly terminated" (Issue https://github.com/OpenJML/OpenJML/issues/792)
  2. The file ajml/examples/SortedInts3.java works, but lines 6, 13 and 27 are not being verified (commented) because I faced problems using the keyword "owner" (Issue https://github.com/OpenJML/OpenJML/issues/797)
davidcok commented 1 year ago

Please log issues for examples in the documentation that do not actually work.

marcel139 commented 1 year ago

The vast majority of them worked as they are presented in the documentation (excellent documentatio by the way). I would be happy to log issuea for them, but unfortunately, I didn't registered which ones needed some work :-(

Em qua., 8 de mar. de 2023 21:26, David Cok @.***> escreveu:

Please log issues for examples in the documentation that do not actually work.

— Reply to this email directly, view it on GitHub https://github.com/OpenJML/OpenJML/issues/800#issuecomment-1461077073, or unsubscribe https://github.com/notifications/unsubscribe-auth/AB65KFRTBBFXCIDSNKFPW7DW3EPRVANCNFSM6AAAAAAVUNGDD4 . You are receiving this because you authored the thread.Message ID: @.***>