Mutable data structures library

[jorge-jbs]

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:

• Lists: implemented with doubly linked lists and with arrays.
• Stacks, queues and deques: with linked-based and array-based implementations.
• Maps, sets and multisets: their specification and implementation is currently experimental. We are working on their implementation based on red-black trees.

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]

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]

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]

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 dafny-lang/dafny#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.