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 Homer

Published in

Workshop on Formal Techniques for Java-like Programs (FTfJP), 2024

The final copy of this publication is available from the publisher.

Resources

PDF
mwh.nz/pdf/ftfjp2024
this page
mwh.nz/pubs/ftfjp2024
Michael Homer — 2024 e6b1d5c8