search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Mutable data structures library #102

Open jorge-jbs opened 1 year ago

jorge-jbs commented 1 year ago

Hello! As part of my Bachelor's and Master's thesis, @ClaraSegura, @manuelmontenegro and I have developed a library of mutable abstract data types. They are fully verified and specified in Dafny, with no calls to external code. We have taken into account how the user would use our library, so we have an extensive set of examples using the library. We have submitted a paper that explains our work to a journal. It is currently under review, but in the meantime you can check this conference paper, my Bachelor's Thesis or my Master's Thesis. The ADTs that we have developed are the following:

We have specified and verified mutable iterators for lists (although linked list iterators and vector iterators behave slightly differently, which is expressed in their specification). Iterators for maps/sets/multisets are currently very much work in progress, but they are our next target.

We don't know if this code would fit better as part of Dafny Core, as an "official" library in this repository or as a standalone library like it already is in our GitHub repository at https://github.com/jorge-jbs/adt-verification-dafny, so we are open to your comments.

davidcok commented 1 year ago

Thanks for this. We are in the middle of releasing a major release, so give us some time to get back to you. 1) One first question would be: is your code consistent with Dafny 4 defaults and syntax 2) We (at least I) will have some detailed comments on the API itself 3) But the biggest question is for us to settle the question of how to organize various Dafny libraries, wheterh internal or external contributions. But this is a great start.

jorge-jbs commented 1 year ago

Sorry for the delay. Porting to Dafny 4 is in our plans, but we have just recently started with the port. Once it is completed we will tell you. And our paper has been accepted, so when it is published we will share it with you, it will probably answer many questions.

jorge-jbs commented 1 year ago

A little update: the paper is published here, if you have any questions don't hesitate to ask. We started porting to Dafny 4 but got stuck with https://github.com/dafny-lang/dafny/issues/4056. Once the next release is published we will continue with the port. We plan on changing the structure of the library so that it is more user-friendly, so if you have a planned structure for your library maybe we can match it.