Home > Research > Publications & Outputs > The Faultless Way of Programming

Electronic data

  • EuroPLoP 2024 Faultless Preprint

    Accepted author manuscript, 879 KB, PDF document

    Available under license: CC BY: Creative Commons Attribution 4.0 International License

View graph of relations

The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

E-pub ahead of print
Publication date15/11/2024
Host publicationEuroPLoP 2024 Proceedings
Place of PublicationNew York
PublisherACM
Number of pages10
<mark>Original language</mark>English

Abstract

There is one faultless way of programming. It uses computer intelligence to validate computer code: formal verification. Yet for developers this faultless approach has remained alien, incomprehensible, and many miss out on its proven benefits. This set of patterns introduces Dafny to developers. Dafny provides a powerful way to incorporate formal verification into software that is integrated with languages like Java and C#, generating code that is provably free from defects and problems.

The patterns range from the Dafny design philosophy to concepts like ghost variables and implementation details such as the use of generative artificial intelligence. By offering an accessible approach to a difficult subject, they support developers in producing faultless code.