Rustan Leino: Spec# is a research project of we've been doing for a number of years in Microsoft research and it comprises a number of tools: the Spec# language, the Spec# compiler time checker, the runtime checking that you get from that and the static program verifier. To go with all of that we also have some programming discipline that is a number of rules that you can follow for how to write your programs in such a way that you can actually verify it. And so, as a language Spec# is a superset of C# and we add some additional types that are checked statically and we also add contracts such as pre-imposed conditions so that you can describe what you intend the behavior of your code to be.
2. Could you explain what Boogie is and how Boogie actually works?
Mike Barnett: Boogie is the name we use for our static program verifier, that part of the Spec# system which looks at the code before it's executed at compile time and tries to determine whether any of the contracts in the code could ever be violated by any execution path, whatsoever. So as opposed to testing which tells you the execution paths were actually followed and will behave properly or not. The Boogie verifier can give you an assurance there is no possible execution path that could ever go wrong. The kinds of things it checks are built-in meanings in a language, such as that an array access is always within bounds that no null values ever de-referenced and extends to all of the programmer written assertions; such as method preconditions, method post conditions. So if you have a method post condition it says the implementation of that method had better return a value meeting certain condition. Such as it's always greater than three and the Boogie verifier will just look statically at the code and if it gives you the green light then you know that there is no possible way that method will ever return something less than three.
3. What could Spec# bring to software development as a whole?
Rustan Leino: The contract and especially the statically verified contracts can help you at compile time to get your programs to be correct more quickly. It complements unit testing in that case and system tests because you can find errors much quicker in the developer cycle. If you want to do a whole system's test of something then you have your whole program or most of the programs that you can actually test it, but with the contracts and the static clarification that we do you can do it on a class by class basis that is as you've written one class you can catch the errors at that point. As we know the sooner in the development cycle you point the errors, the cheaper they are to fix. So this is shifting that cost to earlier in the project so that you get something that is more reliable later on in the development cycle and get there quicker.
Mike Barnett: It forces you to be explicit about the kinds of design decisions that normally are left only implicitly into the code and then violations of which tend to be found extremely late in the development cycle. We never intended that this could be called in such a scenario but if you have the contracts in place at the API level then you rule out the entire categories of behavior that the API was not designed for and that is now apparent right up front.
4. How would Spec# differ from Eiffel?
Rustan Leino: Spec# is much influenced, of course, by Eiffel and by the JML language which also draws from Eiffel and other sources. Spec# is like Eiffel in that we have pre-imposed conditions and they are checked at run-time so when you compile things you get those runtimes checks. We go beyond where Eiffel is not only in the types we add to the language, but also in that we can provide static verification which is something that Eiffel has never provided. Static verification, of course, also comes at a cost, but the idea beyond the contracts is the same in both cases. That is you write down your intent of the code and you check it either dynamically at one time or statically with the program verifier.
5. Do you stop testing your contractual invariants in your unit tests and focus on your behaviors?
Rustan Leino: Many of things we see in test failures are things being empty, things being null, things running off the end of some buffers, the source of those errors can all be caught using our machinery statically, which means that you wouldn't have to write unit test with those in particular, but typically the specifications that you will write are lighter specifications than trying to specify the full correctness of what your thing is going to do. So they may rely on unit tests, but it could mean that for unit tests we focus some of their effort on trying to test for those behaviors, perhaps, as well.
Mike Barnett: Spec# really allows you to automate the parts of the unit testing that are very mechanical and very repetitive and since a machine can't take care of them. I mean, Spec# demonstrates that it's possible to make those tests not even necessary. It's able to force you to write your code in such a way that those tests are unnecessary, leaving the deeper tests that require a human to write, as the main focus for unit testing.
Rustan Leino: Pex is a really great project. It focuses on testing and doing the testing more deeply in the program by constructing test cases for you. It uses analysis techniques that are similar to ours and in fact uses one of the same engines behind the scenes as we do for analyzing the program trying to figure out execution paths that you would want to try in the unit test. Pex then constructs unit test based on that. The advantage of that is that you get the benefit, you can also use contracts with Pex, so you can get the benefits of getting the test cases from your code and from the contracts and when you run packs.
If something goes wrong you have very concrete evidence that something is really wrong with your code because you are sitting there and something has crashed. What you use Spec# for is similar in technology. You don't need to run your program to run the Spec# program verifier, but what you get is that it will check all the paths. In Pex you would only check those paths that you actually have test cases for, whereas with Boogie, with the program verifier, you actually check all the paths through code. Of course that also comes at half an expense, that it's difficult to verify a program statically and you have to convince a tool that your program is correct, but the benefits are then higher.
Mike Barnett: And the two tools actually work really well together. We worked with the Pex team and one of the difficult problems Pex has to face is its' trying to explore the states base that a program could be in. So it's trying to explore lots of different execution paths in the program and when there are contracts in that code the contract serves to prune the search space and so it makes Pex more efficient when it's analyzing code that has contracts in it.
Rustan Leino: Yes we have. Initially we've done an approach where we took a fairly simple tool to mine the code for contracts and tried to construct contracts for the library and we put those into what we call " out of band contracts", which are shadow assemblies that sits side-by-side the real libraries and when our tools read in the libraries they also read in the shadow assemblies and fuse the two together as if the contracts have been in an available form in the library in the first place. So that means that for those we have some contracts for all classes in the library, but they are not all correct and they are not all complete because the tools that we used for were very simple. In discussions with the BCL team, for example, lately I have been trying to actually get these contracts to be more manifest in the code itself so that when we try to use other tools to extract them we could do so accurately and that is something that we hope to see in the .NET library but there is a lot of work to make that actually take place.
8. In terms of the future of Spec#, where do you see it going or where would you like to see it going?
Rustan Leino: One of the things we are facing is that C# evolves and Spec# has been until now a superset of C#, C# 2.0. As C# has evolved into 3.0 and into later versions, we in a research group, don't have the engineering resources to keep up with all those things which means that Spec# is going to remain as a language by itself that will be a superset of C# 2.0. That means it can still be used in education at universities for teaching people about pre-imposed conditions, software engineering, things like that. But evolving into new languages, into new versions of C#, other versions of languages in .NET we're exploring language independent solutions where the contracts that you write in the code are placed in a code in a language independent way, in such a way that our tools can still fish them out and do good things with them.
Mike Barnett: I think the mission of Microsoft research is two-fold; it's to provide whatever input we can to product groups and it's also to participate in cutting-edge academic research. I think of Spec# as a separate language all by itself that will continue in academic research. There are a lot of topics we'd still like to do research on for object oriented verification. But we've always tried to find ways to peel layers off that that can be adopted by different product groups.
9. If I wanted to use Spec#, what are my currently available options?
Rustan Leino: The first thing you should do is go to the Spec# website and download the Spec# distribution which comes for free and with that you can use the Spec# language as another language in Visual Studio and then you get the special Spec# mode that we provide there. There is also another use of it that is you can use the Spec# specific features as add on things in the C# program. So once you've installed Spec# you can set the properties of your C# projects such that they will make use of contracts. Then we will run our compiler on the C# projects and dig out additional attributes from markup in the program that to the C# compiler looks like comments.
We dig them out and read them as contracts or pre-imposed conditions. That means that there is a way to use C# today with contract features, run our compilers and still get the benefit. If you don't like it, you pull the plug immediately and turn off the contract features and your C# program is still there. To use Spec# right now, one needs to limit themselves to the C# 2.0 features since we do not support the 3.0 features of this point.
Rustan Leino: We don't know exactly. It's hard to say before you've actually done it, but it seems that most of the features there are syntactic sugar for a bunch of nice things that is the link features and so forth. The equal-like queries and things like that and as long as our compiler would see those as the IL they would generate, we can presumably handle them, but maybe there are additional specifications that one could write. Especially for these types of things and to explore that we really need to come and jump in to it and explore it. Otherwise just to compile from the source code into the IL so that we can add our contracts in there means that we need to extend our compiler to those features and that is a big engineering effort, but we don't anticipate any large research problems with the new features.