Specification and Verification: The Spec# Experience
Reviewed by Greg Wilson / 2011-06-30
Keywords: Experience Reports, Formal Methods
Barnett2011 Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter: "Specification and verification: the Spec# experience". Communications of the ACM, 54(6), 2011, 10.1145/1953122.1953145.
Spec# is a programming system that facilitates the development of correct software. The Spec# language extends C# with contracts that allow programmers to express their design intent in the code. The Spec# tool suite consists of a compiler that emits run-time checks for contracts, a static program verifier that attempts to mathematically prove the correctness of programs, and an integration into the Visual Studio development environment. Spec# shows how contracts and verifiers can be integrated seamlessly into the software development process. This paper reflects on the six-year history of the Spec# project, scientific contributions it has made, remaining challenges for tools that seek to establish program correctness, and prospects of incorporating verification into everyday software engineering.
A plethora of testing tools and static analyzers "suddenly" became mainstream a decade ago after years of hard work and experimentation by their creators. Today, program verification tools are poised to become part of every serious developer's toolbox in the same way, not least because of the challenges of concurrent programming. This experience report describes what a mature verification tool can do, and what its creators learned while building it and trying to persuade people to adopt it. Even if you're not using C#, it offers a lot of insight into things to come.