Spec#: Contracts for C# and Then Some

Spec# (pronounced "Spec Sharp") is a programming system from Microsoft Research that, among other features, adds contracts to C#.

According to its developers, Spec# attempts to streamline the development and maintenance of high-quality software. "Our goal," say Rustan Leino, Mike Barnett, and Wolfram Schulte is to move "normally skilled programmers to a higher-integrity language" by adding specifications to their software. The system consists of the object-oriented Spec# programming language, a Spec# compiler, and the Boogie static program verifier.

"What we’ve tried to do," says Leino, the project lead, "is think about the whole experience of the language. How do you write the programs? What sort of specifications do you include in the programs? What do you do with them?

"The overall goal is to improve the software-engineering process," Leino goes on to say. "Software engineering is very expensive in terms of figuring out and designing what the program should do and then actually writing the programs. There’s a lot of cost in writing the programs up front to develop them initially. But a much larger cost is the maintenance of the program.

"What we’d like to do is make it more cost-effective in various ways. Programmers tend to run tests, so the testing accounts for a large portion of the cost of software engineering. That is, in some sense, what we’re competing with, but we’re not aiming to replace testing. We just want to be able to do it in a smarter way earlier in the software-development cycle, and the way to do that is to use specifications."

To make all this possible, the computer scientists focus on three issues:

• Type checking
• Pre- and post-conditions
• Program verification.

What's unique about Spec#'s approach to type checking is how it checks for non-null types, to make sure that pointers within a program point to the objects for which they are intended. "When the compiler runs, says Leino, "the programmer gets that checking immediately."

In terms of pre- and post-conditions, Spec# resembles the Eiffel object-oriented programming languages. Like Eiffel, Spec# provides runtime checking of preconditions and postconditions. Leino explains: "The programmer, by writing down just one precondition in the entire program -- or two or three or 100 -- gets the benefit of our compiler generating runtime checking.

And when it comes to static program verification, Spec# analyzes the program mathematically to check that these specifications really always hold. That means that you need to have enough specifications in the program that you can convince even a program verifier that the program is correct.

As its "#" suggests, Spec# is a superset of C#, which means that it should be straightforward for C# programmers and Visual Studio users to adopt. While not as fully featured as Visual Studio overall, Spec# does provide additional quality checks thanks to contracts.

"Those can be put in a C# program as just comments," Leino explains. "That means that when the C# compiler looks at the program, it ignores the comments. But when the Spec# compiler runs on the same program, it looks into the comments and treats them as if they weren’t written in comments. C# programmers can download our system and choose to turn on contracts. If they do that, they can write contracts in the comments. Then, when they compile it in Visual Studio, they can first run the C# compiler, then immediately afterward run the Spec# compiler. Then they get all the whiz-bang features of C# and the benefits of our compiler."

Spec# also offers runtime checking for object invariants. An object invariant is a condition that describes the steady state of a program’s data structures, something difficult to verify statically. Spec# addresses this concern by utilizing modular checking, in which the program is analyzed bit by bit, one piece at a time. By taking a look at each piece of a program, the whole can be verified.

"Smoothing out the experience of using the system is a thing that we’re working on,” Leino says. "Trying to improve error messages or give more detail, and expanding the methodology to be able to handle more common programming idioms. Increasing the power of the specification language in certain ways. Improving the theorem-proving technology to make things faster and more effective."

For more information, see The Spec# Programming System: An Overview.

Posted by Jon Erickson at 09:39 AM  Permalink