Home

Specification and Verification: The Spec# Experience

Mike Barnett, Manuel Fahndrich, K. Rustan M. Leino, Peter Muller, Wolfram Schulte, and Herman Venter, Specification and Verification: The Spec# Experience" Preprint of an article appearing in the June 2011 CACM.

CACM tagline: Can a programming language really help programmers write better programs?

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.

Spec# is, in some ways, quite similar to JML+ESC/Java2. But Spec# is a language rather than a set of annotations, which allows it to incorporate features such as a non-null type system and a very tight integration with the IDE.

Spec# was previously mentioned on LtU back in 2005.

By Allan McInnes at 2011-06-01 06:11 | Implementation | OOP | Software Engineering | other blogs | 14421 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Very interesting indeed

The following paragraph made my day:

Third, a conclusion we have drawn from our interaction with developers is that real developers do appreciate contracts — contracts are not just an esoteric feature prescribed by “Dijkstra clones”. Unfortunately, we have also seen an unreasonable seduction with static checking. When programmers see our demos, they often develop a romantic enthusiasm that does not correspond to verification reality. Postinstallation depression can then set in as they encounter difficulties while trying to verify their own programs.

The article is full of "this would be too much work" remarks about support for some language features (eg. features added in new C# versions), or tooling support (keeping up to date wrt. new features of the C# IDE integration). While they reasonably look like "insiders" of the Microsoft language development chain, they are still external to the projects they were building upon, and seemed to have encountered environment support problems not dissimilar to the usual pure-academia languages. I'm wondering what could lower the cost of such attempts, short of integrating those language features into the base language (or, here, all of .NET languages?) directly.

By gasche at Fri, 2011-06-03 09:59 | login or register to post comments

Good question

I'm wondering what could lower the cost of such attempts, short of integrating those language features into the base language (or, here, all of .NET languages?) directly.

Good question! (I have the same :)

By Cyril at Fri, 2011-06-03 17:36 | login or register to post comments

No mention of Singularity or Midori

It's interesting to note that the paper makes no mention of Sing#, Singularity, or Midori (a Singularity descendent), other than a dangling reference in the glossary that I suspect reflects a redaction error.

Now a very important question to ask here would be: does Midori use Spec# or Sing#, and if not, why not? Given the explicitly stated goal to be useful for "real programs", the absence of any mention of these relationships and their outcomes is cause for skepticism.

By shap at Fri, 2011-06-10 04:46 | login or register to post comments