search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.84k stars 254 forks source link

Standard library: MutableCollections #4648

Open robin-aws opened 8 months ago

robin-aws commented 8 months ago

Mutable versions of common collection types.

~Depends on #4640, since the current approach is using {:extern} to use efficient native implementations.~

Update: starting with Vector from the existing JSON library, since it is pure Dafny that doesn't need extern code

Existing source:

~dafny-lang/libraries/src/MutableMap (partial)~ - Paused since the Go and JS backends don't support hashcodes on all Dafny types, so it's not possible to implement efficiently yet dafny-lang/libraries/src/JSON/Utils/Vectors.dfy

robin-aws commented 8 months ago

Note that the current implementation's example makes use of a generic AssertAndExpect utility that should be promoted somewhere more central.