Dafny vs. Dala: Experience with Mechanising Language Design
Abstract
Dala is a design for a concurrent dynamic object-oriented language. A key goal of Dala’s design is to avoid data races, by ensuring threads do not share mutable state. In this paper we discuss our experience using the program verification tool Dafny to validate Dala’s design. We explain how we modelled salient features of Dala in Dafny, and how Dafny did (or did not) assist our confidence in Dala’s design.
Authors
James Noble, Julian Mackay, Tobias Wrigstad, Andrew Fawcet, Michael HomerPublished in
Workshop on Formal Techniques for Java-like Programs (FTfJP), 2024The final copy of this publication is available from the publisher.
Resources
- Author copy (PDF)
- mwh.nz/pdf/ftfjp2024
- this page
- mwh.nz/pubs/ftfjp2024