Library of formally verified abstract data types in Dafny.
This work aims to specify, implement and verify common types
of collections, like those found in C++ or Java standard
libraries. These collections are specified as abstract data
types, they all extend the ADT trait. Each of
them can have different subtypes for different expected behavior
(e.g., ArrayList and
LinkedList both extend
List). Notably, we have made sure to
completely specify the behavior of iterators, which differs between
different ADTs.
All the implementations of the library are formally proven to respect the specification, thanks to Dafny. Compilation to other languages is planned.
The specifications are designed so that client code that uses them can:
- Have basic security guarantees: the collection is valid and is not shared.
- Give formal specifications of the functional behavior of the code: like proving that a method that reverses the order of the elements of a list actually reverses them.
- Reason about the state of iterators to maintain their invariants and, thus, prove that the code is correct.
In essence, this library allows you to perform the same operations as in the C++ library, but no unexpected behavior can occur since you can formally verify that your code uses the implementation as specified. On the other side of the spectrum, you can use the ADTs of this library without doing any verification, and it is guaranteed that the collection types of this library will not be a source of bugs.
Currently, this library is under development and is not documented. If you want to use the library we advice you to wait until it is better documented or to check the related research of the next section.