By Rob Knies
August 14, 2007 8:00 AM PT
Modern-day software development is notoriously challenging. Programs have become highly complex. Customer expectations have never been higher. Meeting quality standards is increasingly difficult.
Challenging, yes. Difficult, perhaps. But such hurdles are not insurmountable, as Spec# demonstrates.
Spec#, available for download, is a programming system devised by researchers from the Programming Languages and Methods group at Microsoft Research Redmond. The project—started by Rustan Leino, Mike Barnett, and Wolfram Schulte—attempts to streamline the development and maintenance of high-quality software.
“Our goal,” the three write in a paper entitled The Spec# Programming System: An Overview, “[is to migrate] normally skilled programmers to a higher-integrity language.”
And just how do they propose doing that? Try the carrot-and-stick approach—but hold the stick. Spec# is an effort to encourage programmers to add specifications to their software, to ensure that the assumptions that are made during the software-engineering process hold true. And the system—consisting of the object-oriented Spec# programming language, a Spec# compiler, and the Boogie static program verifier—provides incentives for the adoption of such techniques.
“What we’ve tried to do,” says Leino, the project lead and a principal researcher with the Programming Languages and Methods group, managed by Schulte, “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?”
Those are the questions the Spec# project attempts to answer, but the goal is to improve the process of writing high-quality software.
“The overall goal is to improve the software-engineering process,” Leino says. “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.”
The idea of appending specifications to the software-engineering process is not new. Such techniques have been discussed for decades. But it’s been an uphill battle to get software developers to embrace the concept of building specifications into the development model.
“It takes more of a long-term view to understand why the specifications are good,” Leino concedes. “Typically, if you have to do a lot more up front to develop the program, then many people in the process get nervous, because they’re not getting as quickly to the date when testing starts.
“The idea is that if you do these things up front, it takes you longer to get to that point, but when you do, the program is in much better shape to begin with. Having the specifications in the program means that when you maintain the program, someone can come in, read the specifications, and when they make changes, you can immediately have tools that check to make sure you haven’t messed up anything in the program.”
The concept is sound, but how can it be implemented within an environment that values go-to-market alacrity?
“To communicate that benefit to the programmer,” Leino says, “we must give them incentive to do it.”
Enter the carrot. In this instance, the incentives take three forms. The first is type checking, which occurs during program compilation.
“The programmer writes the program in some language—in our case, Spec#,” Leino says, “and then wants to translate it into something the machine can actually run. When the compiler runs, it also involves a type checker, which is a very coarse-grained way to look at the program and figure out that you’re not mixing up apples and oranges, integers and Booleans.”
Type checking has been used in all modern programming languages, so software developers are quite familiar with that process. What Spec# offers is a way—in large part due to the efforts of Manuel Fähndrich, another Microsoft Research Redmond researcher—of checking for non-null types, to make sure that pointers within a program point to the objects for which they are intended.
“Our type system in Spec# addresses that,” Leino says. “When the compiler runs, the programmer gets that checking immediately. That, we think, is one incentive for them.”
Another is pre- and post-conditions, which represent contracts within a program that ensure that the routines in the program run as expected.
“Think of it as there’s someone who’s going to call a particular routine, and there’s someone who’s going to implement the routine.” Leino says. “You have a contract sitting in between that says what the obligations of the caller are and what the obligations of the implementer are. The caller has to live up to the precondition, but then the implementer can assume that the precondition holds, because the contracts says that it does, and the implementer must establish the postcondition, and then the caller can assume that it holds upon return.”
In its use of such contracts, Spec# resembles the Eiffel object-oriented programming languages. Like Eiffel, Spec# provides runtime checking of preconditions and postconditions.
“The programmer,” Leino says, “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. The programmer starts to benefit.”
The third carrot involves static program verification.
“That means we’re going to analyze the program mathematically to check that these specifications really always hold,” Leino adds. “That process essentially means that you need to have enough specifications in the program that you can convince even a program verifier that the program is correct.
“That step takes a lot more effort for the programmer, so one of our research aims is to provide as much of the boilerplate as we can and to infer things when we can and make it as easy as possible for the programmer to do that last step well. We have lots of research to do there.”
Leino previously worked on a similar static verifier for the Java programming language. But, he hastens to add, Spec# has leapfrogged Eiffel and Java.
“What we offer that is much stronger is the static verification,” he says. “I think we lead there.”
The Spec# project got started about four years ago.
“Wolfram and Mike came from a background of doing runtime checking and modeling in programs,” Leino says, “and they wanted to see contracts in the language. I came more from the static-verification background. We noticed that we had similar interests and then started the project.”
Spec# is aimed at two distinct audiences.
“The people who are using it now and who we would want to be using it are early adopters,” Leino says, “someone who’s willing to try something new, see how it works out. We have an external Spec# mailing list where we get many good questions.
“Another kind of user that we want is users in academia being able to use our language and our tools in teaching, both for students to be able to put in the contracts and get a feeling for what the contracts are for, and then also taking the extra step for verifying statically.
“When specification and verification are taught at universities,” he adds, “the typical way that they’re taught is that you have some lectures and then you learn how to do proofs and loop invariants and pre- and post-conditions. The students do it on paper, and they prove it. They may or may not get it right, they hand it in, and a week later, someone grades it, and then it gets forgotten.
“When they take the next programming class, when they’re sitting at a terminal actually writing a program, they don’t necessarily associate what they did in that paper-and-pen class with the actual programming experience. We think the tools we have can connect those two, so that you both understand the things you’re doing and you’re getting used to putting the things in—pre-conditions, post-conditions—when you’re writing the program.”
Another benefit to Spec# is the fact that the language is a superset of the popular C# programming language.
“If someone is used to programming in C#,” Leino says, “it should be straightforward for them to switch to Spec#. The Spec# compiler accepts C# programs, since we’re a superset of C#, and in Microsoft Visual Studio, you can switch to the Spec# mode, which offers some benefits.”
Of course, because Spec# is a research project, it doesn’t offer all the bells and whistles of Visual Studio. But Spec# does offer the additional quality check enabled by the 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, a particularly thorny programming challenge. 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.
“We see that as a crucial thing in program development,” Leino says. “The way we’ve addressed it is that we have developed a number of rules. We call it the methodology, a discipline for how to program and how to write these object invariants. That was also one of the initial ideas that really got things started about how to undertake this project. We’ve built lots of things on top of that since.”
Four years, obviously, is a long time to continue working on a single project. But Leino says it has been time well spent.
“Even though it has been one project,” he says, “there are many different technical portions of it that have come in stages. There’s some portion of it that we would want to explore in some way, so we explore that, and then we move on to the next part or maybe come back to some portion of it. Of course, as those years go on, the whole system becomes better, as well.
“From a research perspective, there are certainly lots of things still to explore. What we’re trying to do is continue exploring in the context of Spec#, but we’re also starting to apply similar techniques to verify C programs. I also have an interest in trying to do it with functional programs or dynamically typed programs. We’re not at the stage where we say: ‘Well, that was it. We’re done.’ There are many interesting things to usefully explore.”
“Smoothing out the experience of using the system is a thing that we’re working on,” Leino replies. “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.
“Some of the next steps that we’re also involved in is trying to have an influence on the .NET Framework and other languages. Could we roll in the non-null types into the C# language? Having the contracts in the .NET library, in a way that tools can make use of it, is also something that we’re working on actively with the people in that group.
“If those things come together, then some of the current and next steps involve trying to take pieces of our technology from Spec# and trying to roll them into the Common Language Runtime, the .NET Framework, and languages like C#. We see Spec# as the research vehicle for exploring things, and the things that work out in a nice way we then hope to transfer into a product.”
Over the past few years, the project has benefited from the help of a number of colleagues, including Herman Venter, Francesco Logozzo, Peter Müller, and a succession of interns. It’s clear that the passion for Spec# remains unabated.
“One of the things that got me interested in the first place,” he recalls, “was that, before I went back to graduate school, I worked at Microsoft as a programmer. I had great fun, and our group used contracts, and we found that we were able to have a much lower bug count than many other groups. Many of the errors we found were because of a broken contract.
“When I went back to graduate school, that interested me, to say, ‘How can you take those specifications and check them statically?’ That’s a bit of what got me into this, and that still has me jazzed up, the idea that we could change the way programming is done. That vision, that such systems would be on every programmer’s desktop in languages like Spec#—that’s certainly what’s driving me.”