On July 1st, 2010, I had the pleasure of spending an hour with Microsoft Code Contracts team members Mike Barnett and Manuel Fahndrich. This article provides a transcript of the interview and a podcast so that you can read and hear first-hand as Mike and Manuel answer some common questions about Code Contracts.

The Participants

An Interview Recorded at 9:40 am PDT on July 1, 2010

If your browser is HTML5 audio capable, you should see controls above to listen to this podcast. If not or if you're reading this post via syndication or if you just want to download it for later playback, you can get this podcast in Ogg Vorbis format or in MP3 format.

[Kevin@00:02] Welcome to the Developer Journey Podcast, my name is Kevin Hazzard. I'm a Microsoft C# MVP and I'll be your host for the show today. Our guests today are Mike Barnett and Manuel Fahndrich of Microsoft Corporation. Mike is a Research Software Design Engineer at Microsoft and Manuel serves as the Senior Researcher on the Microsoft Code Contracts team. Welcome to the show.

[Manuel] Thanks.

[Mike] Thank you.

[Kevin@00:27] Let's just get started by talking about what you guys do. The title for example, Mike, Research Design Software Engineer, what does that mean at Microsoft? What do you do? What's your day like?

[Mike] So, in Microsoft Research, there's two main job titles: there's Researchers and there's Software Design Engineers. The difference between the two is very flexible. It depends on the group that people are in. So, in our group, we tend to be more project oriented. People do whatever's needed to work on the project. But in general, Researchers tend to be more research paper-oriented, perhaps, and academically-oriented and the developers are supposed to be a little more coding-oriented but in our group that's just not… I mean, Manuel probably bangs out at least twice as much code as I ever can write. So we're not real big on titles and we're not real big on distinctions. We just try to get the work done.

[Kevin@01:22] Sure, that makes sense. Titles often don't tell us what people are all about. So, Manuel, I see that you are very active on the Social MSDN site where there's a lot of threaded discussions about Code Contracts. So, you're writing code, as Mike says, you're out there cranking out code but you're also very active in the community, as it were, talking about Code Contracts. What's your role on the team? And I'd like for you to talk for a minute about your interaction on the Social MSDN site and what developers seem to be excited about with respect to Code Contracts and how they're responding about the release of the product into the framework.

[Manuel] Sure. So, I see my role as basically making sure that all the loose ends get tied up and just driving the whole project forward, figuring out what needs to be done and making sure it gets done somehow. The MSDN site has been really useful for us in terms of getting feedback from actual users, not just being a project that we think is cool but no one else cares about. So having feedback and actually being told, well, "this needs to be different" or "you haven't thought about this issue" and so on has been very, very useful and we've actually included a lot feedback and change to design over time to accommodate things that have been brought up in the forum. So we're very grateful to all the users there and all the feedback we get. I try to be active there, try to figure out what's working and what's not working and figure things out on our side to help them. So, yeah that's what I see the social aspect of the forum is good. And I think the feedback overall, I would say, has been overwhelming positive in that people do get excited about having a common way to write contracts in their code that are supported by a set of tools. And I think the fact that the authoring part of the contracts, namely that you can write them is now in 4.0 is really helping a lot because people can just start authoring them without having any dependencies on extra libraries and so on and I think that makes a big difference.

[Kevin@03:42] Well, that's good. It's good to hear that people are open to the idea of contracts in code. Which leads into my next question. Some of our listeners and readers are familiar with the concept of contracts in code because they read blogs and they watch podcasts or listen to podcasts and they track things in the business. For example, I know a lot of people just routinely visit the Microsoft DevLabs and Research sites just to see what you guys are working on. And they'll pick up on a project like Code Contracts and find out that there are really interesting things that they can do within their code. But a lot of people don't necessarily know what Code Contracts are or they're not familiar with Design-by-Contract languages like Eiffel or Spec#. And I was hoping that you guys could take a minute to minute to initiate people who don't really know about Code Contracts and what they are and relate that to how they came into being at Microsoft. Why did you guys decide to create Code Contracts?

[Manuel] Whoa! That's a big question. I guess there's a lot of reasons and a pretty circuitous route how we got to where we are today. Let me just give you a perspective maybe from my side and then maybe Mike can fill in some of what I'm missing. So my background is actually more in static program analysis so the tools that try to find errors or prove certain things correct in your code without running the code. And one of the problems that one runs into in that field is always that if you don't specifications about what the code is supposed to be doing, then it's kind of hard to do this static analysis. And that has several aspects. One is: you have to know what needs to be proven. The other thing is you need to break down problem of proving an entire program correct into smaller, manageable chunks and so, if you write specifications like contracts that are expressing the conditions and boundaries of methods like preconditions and postconditions, it makes this whole problem more manageable because it breaks it down into smaller pieces that can be done. And, so one of the motivations from a long time ago that brought us onto this trajectory was essentially having such specifications to make static analysis more amenable. But, I think over time we now found that that's a good thing to shoot for but it's not necessarily the first thing one wants to do. In fact, we now tell the story that you should write contracts to document your APIs first and foremost because you're never the only person looking at a piece of code or using a piece of code so having this kind of documentation is very useful. And then, once you write that down in a way that machines can actually understand it, it's not just a comment, you can enable tools like the runtime checking that actually enforce these contracts at runtime. And then, starting on that route if you have a lot of contracts and you want to tie down the correctness of a particular piece of code, you then may want to start trying to use the static analyzer and really get into the very depths of writing specifications.

[Kevin@07:11] What's interesting is when I talk to people about Code Contracts, I'll actually avoid the word documentation during a presentation, for example, to a user group or a Code Camp or something like that and almost invariably within ten minutes someone in the audience will recognize, "Hey, this is like documentation!" And that's when the light bulb goes off. I can tell that person gets it because we've got this way of expressing a documentation comment, almost, that's machine readable. Is that a good way to think about it?

[Manuel] Yeah, exactly.

[Mike] I think if you look at it in the broad context that happened in the history of computing, there's… the trend has always been toward making more things that are machine checkable. So in the early days when we just did assembly-level programming, there weren't even types, right? You just passed registers or values. And typed languages made this huge advance where all of a sudden the compiler could give you this benefit by not allowing you to even compile a program that had certain errors in it such as treating an integer as a string or treating a character as a number. Of course, then there are certain restrictions that come with that and then people fight with those but overall I think most people agree that having a typed language is a really great advance and so contracts are… You can think of it as enriching that type signature so that now you know not only when you call this method that you need to give it an integer but you know properties about the integer you need to pass it.

[Kevin@08:45] Very good. So let's jump from here and talk a little bit about the tools. The tools that ship with Code Contracts come in a variety of forms. And maybe you could take a moment to talk about runtime tooling and tooling that's available inside Visual Studio. And then maybe differentiate if you can about what pieces had to be put into the CLR to support this and the kinds of classes in the framework to support it as well.

[Mike] OK, so what ships currently in .NET 4.0, the only thing that's in the framework is the Contract class itself which is a class with several static methods such as Requires and Ensures that allow you to write these specifications as part of your .NET program. And because it's a library, it means that you can write these methods no matter that the .NET language is that you're using. So whether you're writing your program in C# or VB, you still call these methods and the expressions you're passing are written in the language that you're writing your program in. So that's the only thing that's actually in the framework. Everything else is an external tool that we've developed here in Research just to show what kinds of things that can be done once everyone agrees upon the standardized encoding of Code Contracts. And so the tools that exist so far are Visual Studio integration, so that your project properties have a pane that lets you control the rest of the tools. And then the tools it controls are the runtime checker, the static checker and the documentation generation.

[Kevin@10:24] One of the questions that comes up all the time for me is, "Why didn't you make extensions to the C# language or the VB.NET language or any other language to support this?"

[Manuel] Well, I think this is not an either-or question. I think, I mean we obviously tried the language route first. So, I mean, you mentioned Spec# in the introduction and so that was a language for… it had first-class syntax for contracts and so on. Over time, we noticed that first of all, starting with a new language is really difficult because people don't necessarily want to change what language they're programming in, right? Adding a feature like this to an existing language like C# or VB, that takes a lot of effort. There needs to be a really good case for extending a language. And, you  know, the language designers want to see the benefits first but how can you show that without having the features there in the first place? So you go through a chicken-and-egg problem there. So the approach we took with Code Contracts which is solely based on libraries and external tools which doesn't need a language change because effectively, to do that step first, to show OK there is demand, there is all these… there are all these cool tools once you have this. And now it doesn't preclude a language like say C# or VB to say, "Hey, yeah we want to give you nicer syntax for this." Right? They could do that and simply emit whatever format we already have. And then the tools can take advantage of that just as well. So I don't think it's an either-or, it's really an evolution, I think. We could… we now have things in place and if the languages want to follow suit and actually give you nicer syntax, they're free to do that.

[Mike] The benefit about… the other benefit about doing it this way is that it's immediately available to all .NET languages whereas if we had gone the language route, we would have had to maybe do one language at a time and then only the people who program in that language would get the advantages.

[Kevin@12:25] Sure. Obviously, being able to do this immediately for C# and Visual Basic in particular is fantastic without having to negotiate, as you said, all of the things that are necessary to modify a language. You know, languages have inertia and it works both ways. Objects in motion like to remain in motion and C# and VB have their own trajectories at this point.

[Manuel] That's correct.

[Kevin] So is Spec#, in particular, is the current shipping version of Spec# taking advantage of the framework classes in 4.0 or the framework class, the Contract class that you've exposed, for example? Or has it… is it still proprietary in that respect?

[Mike] A couple of… so one, Spec# is now… we released that as open source. That's now on CodePlex as specsharp dot codeplex dot com. And it's existing implementation is still the same as it was when we released it but we have plans to modify it so that it integrates with Code Contracts and uses the Code Contracts infrastructure instead of its own… instead of what we did originally which was an ad hoc, custom infrastructure for implementing the contract support.

[Kevin@13:44] That's good. One of the other big questions I get when I talk about Code Contracts is, "Why did you choose to do this as code?" There are some competing frameworks in other languages like Java, for example, there's a Contract4J package that uses metadata to mark classes and methods up rather than writing what looks like code inside the functions. So, in the .NET space, of course, we would imagine putting attributes on a class or attributes on a function to specify the contracts. Did you all play with that sort of interface early on or was it dismissed out-of-hand as not being a viable option?

[Manuel] I love that question. I think it's definitely a question we get a lot, too. And we did put a lot of thought into it and we had a lot of experience over many years with other approaches, in particular attributes. So, basically attributes would be an ideal system if they were richer to express what you need to do. The problem is that attributes are very restrictive in what they can say and what they can refer to in the code. Unless you want to start encoding full expression languages, you end up having to use, essentially, strings in your attributes to do that which means you now have to define a new language for that, you have to teach it to people. You have to compile it. You have to analyze it and so on. Whereas if you take the approach that we took just writing it in code, you already have the language. It's given. It's the language the programmer is writing in. You have the translation and the semantics of the… those expressions. It's the language compiler that you're using. Which basically takes away a lot of duplication you would otherwise have to do if I start encoding everything as strings in my attributes. Another approach… another advantage of not using attributes is that once your in the attributes with just strings, you have the same problem as if it were just a comment because you now… say you refactor a method and you rename a parameter, right? Well, it won't rename that string which is in the attribute for that parameter but if it's in the code, like it is today, it will rename it properly. So, you get a lot of integration from your existing IDE if you write contracts as code whereas if you write them as attributes or doc, you won't get any of that.

[Kevin@16:19] I had the experience of writing an attribute-based security token analyzer that used Aspect-Oriented Programming in the past and you're exactly right. We had to invent a syntax and teach everyone how to use it and it was very painful. So it makes sense why you chose that path. So, the next question I have is about the tooling again. The static checker is really only available to users of the premium version of Code Contracts. You have a premium version and a standard version, I think you call it. And this means that the static checker is available to the users of the premium and ultimate versions of Visual Studio. Is that correct?

[Manuel] That is correct.

[Kevin] Now the thinking behind that was… I'm trying to get an idea because people ask me this all the time. They like Code Contracts enough that they would consider upgrading. So, it makes me wonder was the thinking behind the decision so that you would essentially drive people to the premium and ultimate editions of Visual Studio. Or was there an assumption that the people that would use the Code Contracts product are likely on the premium edition anyway? Because the static checker, in my opinion, gives a lot of value.

[Manuel] Well, I think there are certainly several aspects of what you mentioned in there. I think, in the end, we are not the business people and we are not making the decisions about how we are going to make money off of this. We like the technology. We're excited about enabling programmers to write better code and so we stay on the technical set and let the… let other people make these decisions. So it's really not… essentially it's not been our decision and we don't really have full control over that.

[Kevin@18:08] OK, so let's get into how the system is used. Developers, when we first get in, developers seem to be genuinely confused about when to use the static checker, when to use the runtime checker. They're two very fundamentally different things, you said before. Static analysis and verification, I sometimes describe as being scaffolding around my code because I can evaluate things at build time. And I think, I have this metaphor in my mind of the runtime checker being a safety net below it at runtime in case things fall or break. They're very different things and developers are looking for some advice about how to think about the static checker generally and how to think about the runtime checker. You have any advice there?

[Manuel] So, maybe I'll just talk a little bit about how we use the tools on our own code base and give you an idea from that perspective. Definitely, if you want to start, if you want to use Contracts, I think the first thing to do is enable the runtime checker. OK, just enable the runtime checker and wherever you think you need a contract, wherever you think about, "Should this be null, should this be non-negative?" Things like that, just write it down as a contract in your code. What you get from that is you basically get early error detection during your test runs. So you think about it, in a similar format, you use asserts in your code, right? These are gates that say, "OK, this shouldn't be happening at this point in my program's execution." And so that way, you effectively augment the number of such checks in your code and hopefully during your testing you will run into them and find errors early on. And at the same time, this will already serve as documentation, right? And so, the good thing about that approach is that you can write as little or as much such specification as you want. There's no cost in terms of you having to write a lot. You can write only what you think should be there.

[Kevin@20:16] That's a good point. You know, the advice I've been giving people is: when you start, you don't have to document everything. You have to start by documenting what you think is important. And come back and add more later if you feel it's important to do that.

[Manuel] Absolutely and that's why I think one should start there. One should start with the runtime checker only. So we've been using the tools on our own code base for implementing the tools, in fact, and so we are using the runtime checker on all the project and we just start filling in these things. Now, when it comes to the static checker, I try to focus my attention on certain aspects, certain parts of the code where I use the static checker. And you can control, for example, using the attribute called ContractVerification, you can control which parts of the code the static checker is actually going to look at. So, I started using those attributes to focus the static checker on some particular classes that I thought were troublesome or maybe had more bugs in the past that other places. And then, trying to really nail down those parts by running the static checker on it and then filling in all the missing specifications that the static checker was pointing out to me.

[Kevin@21:34] How do you do that? Do you start by setting ContractVerification false at an assembly level and then true at a narrow level like at a method or a class level and then working out or do you start from the outside and work in? What's the best way to do that?

[Manuel] Yeah, definitely the first thing you mentioned. So you set it to false on the assembly level and then you start with a particular class or just a method, as you say, and then you work your way out. Exactly, that's what I do.

[Kevin] It's interesting because I worked with a tool years and years ago, when I wrote C and C++ called lint. Lint was a static analysis or verification tool that we could run after the fact or, before actually the object compile to give us hints about things that could be wrong with the code potentially based on some best practices and patterns and things that had been codified over the years. And it was really overwhelming, when you turn lint loose on a base of source code it could generate thousands or hundreds of thousands of warnings that made it almost impossible to get started.

[Manuel] Yeah, I'm familiar with that and this is really a problem with every static analysis and it's no different with the static checker for contracts. If you existing big project and you just let it loose on it, it will overwhelm you. Which is why, I think, you want to start small. You want to focus on one particular smaller class initially that you think it's valuable to do this for and then grow it outwards.

[Kevin@23:06] So, you say start with the runtime checker. As I've been describing, put that safety net underneath. Document only what you think is important and refine that over time. And then, with respect to static analysis, or the static checker, work your way out of an assembly. Start by focusing on methods, then classes and work your way out using that ContractVerification attribute. Is that the pattern you would recommend?

[Manuel] That's exactly the pattern because one thing that happens is if I focus on one particular class, right? I mean that class, the code in that class is going to call other methods from other places, right, that you may not want to run the static checker on yet, right? So you don't but you might still need to write say write some Requires() or Ensures() of these other methods that you're calling. And by using the static checker, it will point some of these things out to you and then by writing those extra contracts on those other parts of your code that you're not running the static checker on, you're now increasing the runtime checking of those parts, right? So, I think that's a good thing. Another thing I use it for, for example, is if you have, you use some library and it has an indexing abstraction, it uses some kind of list abstraction or something like that. And you want to make sure that some piece of code that you want to statically analyze uses that correctly, right? That is that it's always in bounds. Then you can write a precondition, a Requires(), on that other library without doing the static analysis over there and then run the static checker on your code that calls that library and make sure it does the bounds indexing properly, right? So that's kind of how I use it and I think this is really pretty effective so far as long as you focus properly because if you don't focus then you get overwhelmed.

[Kevin@25:00] That's great. That's good advice. I appreciate that. Let's talk for a minute about testing. Another question I get a lot is, "Should I be testing my contracts?"

[Manuel] Yeah, we do get this question a lot. It's an interesting one. I think my reaction is always trying to counter-question first. I mean and like the first kind of question I would ask is, "Are you testing your asserts in your code?"

[Kevin] Well, I typically don't but I guess that's a good question to hand to the people who ask me that question but it really comes down to the code paths that you're going to take and some of those questions that you're going to have to answer early on like, "Am I going to use the runtime support or not?" And I guess if the answer is no, you're not going to be using the runtime support for Code Contracts, does it really make sense to turn it on in a debug build or one that you would execute unit tests against?

[Manuel] Well, we really didn't touch on this aspect yet but I think we should talk about this now about which builds do you want to run the runtime checker on? So I think on the debug build, you should always run the runtime checker. OK, you should always enable that on the debug builds. Whether you want to run it on the release builds or not, now that's a totally different question, right? Effectively, once you release your code, you want to ask yourself, "Well, what checks do I still want to enforce in the release builds?" Right? That is, is it a check that needs to be there because if it's not done something really horrible will happen or if it's not there, well, it's just a bug that, just like any other bug you might still have in your code that might still trigger, you know, in your release builds. So, contracts are not going to prevent problems in your release builds. They'll just point them out earlier. One of the things we have to get into is the issue of preconditions and what happens when the precondition gets, is violated, right? Traditionally, people were told to do parameter validation in the form: check the condition and if it's not true throw some particular ArgumentException or some specialized type from that. And if you do that in your code, your release builds, you really, it's not just like an assert. It's something that you advertise as being functionality of this code. That is your saying, "If you pass me say null, I will throw null exception." And that's a very specific behavior that you are now advertising to everybody and people might say, "Oh, this is great. I'm actually going to rely on this behavior. I am going to catch this null exception and do something in that case." Right? So if you do that, you advertise way more behavior in your code than you might want to. It's very different from an assert. Nobody will rely on an assert. Nobody will say, "Oh, I'm going to hook into the assert handler and if I pass null and this thing triggers then I'm going to do something else." Right? That's not behavior that people will rely on. And with contracts, you have to think of the same things. If you're using preconditions, you have a choice. Do you want this to be advertised with a fixed behavior that is throwing a particular exception that people might rely on? Or do you just want it to be documentation that says, "Don't call me with null?" OK? And what happens when you call me with null is up to me and you cannot rely on any behavior from that point on. Those are decisions that programmers have to make and that will influence how they, what kind of preconditions they write and how they use the tools.

[Kevin@28:45] Yeah, it's interesting. In languages like Java which has the throws statement indicating which exceptions will be thrown by a bit of code, we can see clearly that trying to use that for any kind of enforcement fails most of the time. People will just ratchet up and deal with things at the highest exception level to make their code compile on the consuming side. And so in an attempt to be documenting along the way and somewhat contractual in the way it's specified, we can see that in some cases people are interested in treating those exceptions as part of a contract and most of the time people, consumers of the code, are more interested in treating it like documentation. This is what could happen if you gave me the wrong information, for example, if you gave me a null that I didn't expect. So, I've always thought that the .NET way of handling that, by not really having a throws statement in C#, for example, was good in some respects because it didn't force us to think that, "Hey, this is contractual in nature." But it did leave out a flavor in the language, per se, that gave us a hook for at least expressing it. When you write those legacy style if-then-throw preconditions or if-then-throw statements that we can convert to preconditions with Code Contracts. Before Code Contracts, they were really inside the body of the function that was going to execute and I had no way of conveying that outside of the method. Code Contracts for the first time, give me a way of conveying that. And it's conveyed in a way that the consumer can choose to honor it or use it or not. That's how I look at it. Is that a fair way to look at it?

[Mike] Yeah, oh, absolutely. That's very good.

[Kevin] One of the things that when you talk about the testability of contracts, the first thing that usually pops up is that someone will try to write a unit test around a failing contract, a failure case, and they'll try to put an ExpectedException of ContractException in their unit test. And of course they immediately realize that I can't get this unit test to compile because I can't find the ContractException class. You guys have made that internal. What was your thinking there?

[Manuel] Well, I think we… So, this is really exactly why we had this discussion about what happens at runtime when you violate a particular precondition. Do you advertise a particular exception to be throw or not? Right? And I think, effectively I try to tell people well, if you write your contracts in the form where you have if-then-throws a particular exception or the Requires with the exception argument, then you do advertise what exactly should happen at runtime if you fail this precondition and you say, "Here's the exception that's going to be thrown." So feel free to write tests against that because you are advertising what's going to happen. And that should be the behavior and it should be the same behavior in all builds, right? Now, and for that, you can do it with the existing unit test technology because those exceptions you're going to be throwing are actually the advertised ones and they're not the internal, hidden ContractException. If you use just the Requires, without the particular exceptions, then it's more in the debug flavor I said before, in the assert flavor I talked about before which means are you testing your debug asserts? Are you writing test cases to trigger them? And I think nobody does and I think you shouldn't be doing that either. If you don't advertise what the behavior of a failed precondition should be, then you shouldn't test for it.

[Mike] At the same time, we actually do give people the ability to wire in their own behavior for a failing contract. So if they absolutely… I mean Manuel is pointing out what our position is but we try to also just provide the infrastructure so people can make their own policy decisions. And so there are multiple ways to control the behavior of a failing contract and so if you really do want to write unit tests against failing contracts, you can use those different hooks to control what the behavior is and you can deal with that in your unit tests.

[Kevin@33:10] Are you talking specifically about custom rewriters?

[Mike] OK, so I'm not sure so custom rewriter what I mean is that one part of the tooling is that we allow you to define your own behavior for failing contracts. And those are free to throw whatever exceptions you want or to write things to logs or do whatever behavior you want. In particular they can throw exceptions that your unit tests are expecting to see.

[Kevin] There's a validator, a custom validator. Is that what you're talking about?

[Manuel] No, no, we talking about… You can define… At runtime, right, you can define whenever you wrote a contract, Requires, Ensures and so on there will be a particular method getting called at runtime. Usually, we generate those methods. They're called System dot Contract under underscore ContractRuntime Requires and so on and typically those that we generate automatically for you, those throw this internal ContractException, right, if they fail. Now, you're free to provide these methods yourself in your build. So there's a special option in the settings for the runtime checker.

[Kevin] Oh, yes, without having to do that through a rewriter.

[Manuel] That's right, you can say… Will you have to use a rewriter to make this work.

[Kevin] To wire it up.

[Manuel] Yes, but you can say here's the class that contains these runtime methods, right? And then the rewriter will call, will emit code that calls your methods for all these checks. What you do in those methods is up to you. That is you can check the condition, you can log. You can throw if the condition is not true. You can do whatever you want, right? And so, in fact, obviously for own tools, right, we have to test our own tools and, of course, for our purpose we are testing whether the tools do the right thing, we have to of course check in our unit tests whether the right failure happens for a particular contract, right? For all of them, in fact, right? And so, in order to test that, we use that feature. That is, we have our own runtime failure methods and they throw particular exceptions that we then use in our unit tests, right? But that's different because we're checking the tools. We're not checking the use of the tools.

[Kevin@35:29] Right. So, other than wiring up the custom handlers do you see any other uses, interesting uses, for rewriters that are appearing in the public space? Anybody really using that capability for anything other than that?

[Mike] Sure, there's tons of uses for binary rewriting and there's lots of tools out there in the world that do different things of binary rewriting. But, do you mean relating to contracts?

[Kevin] Yes, relating to contracts.

[Mike] Well, I mean…

[Manuel] We just wanted to make it possible for people if they have this need. We didn't want to lock them out. But I'm not sure if a lot of people will use that feature though.

[Kevin@36:14] All right, so let's move on a bit. Let's talk about the static checker in continuous integration builds. It's something that people ask about and I'm sure you get the question, if I'm using the static checker as you said in the path: start with the runtime checker and graduate to the static checker, but if from there you decide to include it and have it emit warnings that you might want to potentially promote to errors in a continuous integration build. I guess that if your code is solid enough that you've handled everything and you feel comfortable putting the static checker in a continuous integration build, is that something you would even recommend?

[Manuel] Well, we do this in our own continuous integration build and I think once you are comfortable with it and you have your focus of your static checker in a way that makes it work for people, then feel free to use it in your continuous integration builds. That's fine. I suppose you're asking, "How do I make sure my build fails when some new warning comes out?" Is that what you're asking about?

[Kevin] Right, yeah so, for example, in Visual Studio, if you promote warnings to errors, the warnings from the Code Contracts static checker don't seem to get promoted. I've just wondered, myself, if you all did something special to make that true or if it's just because it's running after the compiler?

[Manuel] Well, this is just because it's separate from the compiler, right? So the problem with the treat warnings as errors is ideally this would be something that the infrastructure around all the tools does, for example, Studio. But, in fact, it is not. It is something that… it's an option that gets passed down to the compiler, the C# compiler or the VB compiler and so on. And then the compiler decides, based on that, whether to succeed or fail, right? And we haven't wired that up to our tools because we wanted to make sure, in fact, that we didn't break builds based on things that might come up in our tools because that might be annoying to certain people. So that said, it is still possible to use the static checker as a integration gate, but you have to use… I think there was a blog, there was a post in the forum about this and I think I explained how to do it which is that you have to use the baseline compilation feature which is a way to say, "Here's a set of errors or warnings that I expect form the static checker. Warn me and fail the build if any extra failures happen." Right? And so you can use that feature to actually get the gate going and fail your build if you're not passing those checks.

[Kevin@39:12] Personally, I would not want to break my builds but I get the question from time to time and people seem to want to know one, why doesn't it break the build when you promote warnings to errors today and two, how we would do that. I remember reading that post on the forum about the baseline feature to do that. Is there any plan in the future to potentially wire that into MsBuild so you could promote it?

[Manuel] Well, it certainly would be doable, I think, if there's a big demand for that. Probably we should just keep it a separate option from the warn as errors because that option is really a C# or VB compiler option. It's not a general option, right? For example, that option does not apply to code analysis which is the standard, built in code analysis that comes with Studio. It doesn't apply to that either, right?

[Kevin] Yeah, that's right. OK, I want to talk a bit about coding style and contract architecture. There are different ways to express preconditions. We have the standard Requires call. A generic Requires that takes an exception type which could be thrown and then those legacy style if-then-throw exceptions that you could promote by ending a contract block after them. With respect to the different types of preconditions, is there a recommended pattern for which ones to use? There are issues, for example, around inheritance of if-then-throw style, the legacy style preconditions whereas you might not have those issues using the new style, the ones that are part of the framework Contract class. What advice can you give to people about picking a precondition style based on your runtime, the runtime support you're going after versus what you might be doing at build time?

[Manuel] Well, this is a question that's important and I think we actually have a whole section in the documentation trying to address this issue. I think it goes back to some of the things we discussed earlier. What do you want to happen at runtime in your release build for certain failed preconditions, right? And I think you have to make this decision as a programmer in terms of what am I going to… what behavior do I want there? So I think in the documentation, we point out three scenarios that make sense to us but there are possibly more. So one is… The first scenario, maybe the simplest one is that you say, "I don't care about my release bits, they are not going to throw say particular exceptions for preconditions." Right? If you're in that camp, then you can just use Requires everywhere, the simplest form and you use it on your debug builds but on your release builds, there will be no checking for these. If you do that then that's the simplest approach and you don't really run into any particular problems. The second approach is, "No, I do have some need for runtime failures in my release builds and I want to throw particular exceptions." OK, so now you have a choice, you can say, "OK, I don't want to run the tools on the release build, I don't want to run the rewriter, the runtime instrumenter on the release build." If that's your choice which you might want to do because you don't want to take the risk of adding bad code or something like that to your code due to bugs in our tools, which is a reasonable choice, then you have the issue that you need to use the legacy requires form. OK, you have to use the legacy form and say if-then and then throw the particular exception that you want.

[Mike] And you have to perform contract inheritance manually so you have to go… If you introduce such a precondition in a virtual base method, then in any override you'll need to do that by yourself and add that.

[Manuel] Because the tools are not running, exactly. And so that's why we distinguish that form from say the other form which is the Requires with the exception which you can use if you're willing to run the rewriter on your release builds because then you get the tolling to do the inheritance and so on for you.

[Kevin@43:48] Yeah, that's an interesting distinction that reading some great documentation in the Code Contracts manual but getting to the point where at least I understood early on that inheritance was going to be up to me if I chose the legacy style was something that didn't really jump out of the documentation, I should say.

[Manuel] Yeah, I mean I think this is something we iterated on and found an approach over time because it wasn't clear initially how to solve all these demands from every side. I mean, having to have support for contracts in a way that makes sense even if you don't run the rewriter eventually on the release bits, right? That was always an issue. I think we now came to the current situation because we want to make sure that there's no surprises at runtime in your release builds. OK? That is we don't it to be the case that the behavior in the release build is vastly different with respect to advertised exceptions than in your debug build.

[Kevin] Right.

[Manuel] That's the main point. So if we did the legacy inheritance automatically using the tools, then if you run them… if you run the tools, you might inherit some exceptions and some checks and then you turn the tools off for your release build and now the behavior will be different, right? And we try to avoid that.

[Kevin@45:22] Yeah, that's excellent. Very good. So one of the other things that pops up a lot is that we have a Requires, a generic Requires, of a particular exception type but there's no Ensures of an exception type. What's the reason for that? Is there a plan for potentially changing that in the future?

[Mike] Well, we only have the Requires with the specific exception type to cater to the fact that people were using Code Contracts to retrofit them onto code that had already been written and that had already been advertising these specific exceptions for precondition failures. In general, people had not written postconditions so there, we starting with a clean slate and we can stay true to our ideal vision where contract errors should not be advertising specific exceptions.

[Kevin] Right.

[Mike] The other point for a postcondition is that a postcondition is a failure of the method implementation. And, of course, by the time you ship your code, your code is all perfect.

[Kevin] (laughter)

[Mike] Release builds shouldn't ever have to check the postconditions.

[Kevin] (laughter) That's true. That's true if you're working with a monolithic code base but if you're using Python or Ruby for scripting in the middle of a large rules engine framework, for example, you may not know exactly what the rules are that are going to run… In the middle of something that was statically verified early on. But excellent observation. I was pretty sure that was your reasoning. It is a question that comes up a lot, "Why is there no Ensures of a particular exception, generically, and why is there no Invariant of exception type?"

[Manuel] It's really the same reason that there's no Debug.Assert() with no particular exception.

[Kevin@47:14] That's a good point. We're in the home stretch here. Let's talk a bit about documentation. Now, of course we've talked about Code Contracts being documentation but, of course, there's human-readable documentation that we want to be able to emit. And there is a Sandcastle patch, right, that ships with Code Contracts?

[Mike] One part of the tools that I mentioned early on was the documentation generation and by that… what I means is that if you turn on the XML doc capabilities in your project properties, namely that you're having the compiler generate an XML file that contains the metadata and the information from your triple-slash comments, then your Code Contracts will augment that XML file with custom tags and information about the contracts in your code. Then it's up to downstream tools to make use of that XML. As an example of what could be done, we have as part of the Code Contracts installation, you get a Sandcastle patch that makes Sandcastle's generated documentation contain formatted sections about contracts. The main point is that now we encoded the contracts into the XML file and any downstream tool that processes the XML can take advantages of that.

[Kevin] And those schema changes, if you will, to the XML: are they documented anywhere, other than the patch for Sandcastle?

[Mike] I don't believe so.

[Manuel] That's a good point. Maybe that's an oversight on our part. They should be in the doc, yeah.

[Kevin] I was just thinking about third-party tools, other than Sandcastle, that might want to take the extended XML and potentially consume that to produce their own documentation.

[Mike] Yeah, we should document that. That's a good point. Thank you.

[Kevin] (chuckle) No problem. So, Sandcastle… Let's talk about that for a minute. Do you use that on some or all of your projects?

[Mike] Yeah, we've used it on some projects. We don't often produce externally visible documentation.

[Kevin@49:22] Right, one of the issues when I talk about this to people is say well, Sandcastle hasn't really seen any changes in quite some time and they're worried about potentially support of it in the future. It seems like, with Code Contracts, there's a very good reason for starting to focus on better and more up to date documentation tools. Is Sandcastle going to see an update in the future that you know of? Or do you guys have any plans for a documentation tool related to Code Contracts that might be out there sort of lurking in the future?

[Mike] So we've communicated our patches to the Sandcastle team. I don't know… I don't have any information about what their plans are or whether they're going to update the base implementation to include the contract support. In terms of the future what we've been working on lately and what we hope to release soon is: Visual Studio 2010 has a new extensibility model and a member of our team, Daryl Zuniga, has written several extensions so that you get more documentation in the IDE as you're using it, namely we're enriching the QuickInfo and SignatureHelper bubbles that pop up while you're hovering over a member in the IDE or typing a method call so that you see not only the name of the methods and the arguments and the XML documentation about them but also you'll see the contracts.

[Kevin] Oh, yeah. That's great. That's exactly the kind of thing that I've been looking for. Knowing… We talk about obligations in contracts, right? I have an arithmetic obligation or a non-null obligation, things like that. It would be really nice to see those obligations at the point when you're writing the code.

[Mike] Exactly.

[Manuel] Yep, yep, that was definitely missing so far so we hope to release that pretty soon. And the other thing it will do for you is if you "go to definition" on some library methods, the IDE synthesizes for you the APIs so you can see how they look. And, we augment those, too, so you can actually see the contracts that are there.

[Kevin@51:45] Any time frame on when we might see that extension? And is it going to potentially appear in the Visual Studio Gallery?

[Mike] Yeah. We're hoping to get it out soon, maybe a month, maybe more. But hopefully within the next month and yeah, we would probably put it on the Gallery, I guess. Or it would probably be part of the tools, comes with the install. I'm not sure.

[Manuel] Either way, yeah. Do people use the Gallery. Is that something… how you would find this extension?

[Kevin] Yeah, well I do. A lot of people, now that the Power Tools, the Pro Power Tools and all those are out with updates that are coming rather frequently, the Visual Studio Gallery tools section, in particular, is a pretty hot topic these days.

[Manuel] We should try that.

[Mike] That's what we'll do.

[Kevin] OK, I had one more section I wanted to talk about or one more topic and that is Pex. There is some level of Pex (integration), the Microsoft Program Explorer I guess it's called in the larger sense, with Code Contracts. I was hoping you guys would talk about Pex integration for a bit as a way to wrap up.

[Manuel] Sounds good, yeah. So Pex is obviously another really great tool from Microsoft Research. And there some integration that we've done between Pex and Contracts but, in fact, the nice thing was that we didn't have to do a lot because if you enable the runtime checking, now your code contains contracts and possible failures and Pex automatically takes advantage of trying to find ways to violate them. So that was done in a way that we didn't have to do a lot of integration. Where the integration comes in is the fact that when you say to run Pex on a particular method that has preconditions then the one thing that the integration does for you is that Pex understands what these preconditions are and if it finds inputs to your test methods that violate the preconditions, then it knows that those are not really failures in the test because they are expected, right? Because you're not supposed to pass me that data anyway. And so that's as far as the integration goes on the requires side. The other thing that Pex takes advantage of is that if you write data invariants, using Contract.Invariant methods, Pex uses those to try to synthesize objects that actually try to satisfy your data invariants. So that helps Pex get better data for the objects that it needs to synthesize for the tests that it does.

[Kevin@54:25] Invariants, I've often said that from my perspective as a coder, writing code day in and day out, invariants are a great way for me to make sure that future changes to my code don't break it, don't break obligations or expectations. If I can say that, in general, this is what must be true about the code from a public interface perspective, then attempts to change that are easy to recognize globally, not necessarily within a particular function but for all public methods within the class. And Pex, it sounds like, is really tapping into that… tapping in and looking at it the same way. Here's an invariant and essentially for all the public methods across that class, it could make assumptions about looking for cases to satisfy those invariants.

[Manuel] Yeah, and that's done automatically because simply we instrument the checks for the invariants at all the public methods so Pex will try to violate them and maybe find ways to do that.

[Kevin] So, Pex then… Is Pex looking at the rewritten code to do that or is it looking at the invariant at compile time?

[Manuel] Actually, it looks at the rewritten code and because we instrument everything into the rewritten code, it sees all the checks there automatically.

[Kevin] So I really need to enable the runtime tools to make this work… this integration work well.

[Manuel] Absolutely, so the way to do it is to enable the runtime checking. Yes.

[Kevin] OK. That's great.

[Manuel] We just wanted to point out that there's new website up called www dot pexforfun, in one word, dot com. It's something that Peli and Nikolai put up to enable programmers to play with Pex and contracts. It's just a web interface where you can type a piece of code. It has a bunch of samples as well. And you can submit and it runs Pex on the server and Code Contracts and gives you feedback. So it's a way to play with the tools without having to install them.

[Kevin@56:32] I'm glad you mentioned that because I would have forgotten. I actually found that website yesterday through a friend's… something on Twitter and it tried it out and it's fantastic. So it's P, E, X for fun dot com?

[Mike] Yep.

[Manuel] That's exactly right.

[Kevin] Yeah, that's excellent. It really is a great way to experiment with the tools without having to go through the cost of installing things.

[Manuel] Yes, that's the idea.

[Kevin] Well, that's great. So, that's all the questions I had for today. In closing, do you all want to say anything about Code Contracts and where you guys are looking at going in the future?

[Mike] First off, we would just like to thank you for doing the interview and writing the blog postings you've been writing. And we'd really love to thank everyone out there who's been using it because the entire direction of the project has evolved greatly because of the feedback we've gotten on the forum and from people mailing to us. So that's been great. We're hopeful that in the future, the contract tools will become more tightly integrated into the products and we hope that they help people program better. And get more feedback from the tools to help them make sure their code works better.

[Manuel] Yeah, keep the feedback coming. I think we're very open to hearing what you guys think about Contracts.

[Kevin@57:56] That's great. It's been my pleasure. I really want to thank you all, Mike and Manuel, for participating today and that's it for this show. I'll talk to you guys soon. And as Mike and Manuel said, please visit the forums on the MSDN Social site and give them some great feedback and that will certainly help to shape the product going forward. Mike and Manuel, thanks again.

[Manuel] Thanks!

[Mike] Thank you, Kevin.

[Kevin] Take care.

This blog post is part of a series concerning Microsoft Code Contracts. For a complete series directory, please refer to the following list. Articles without a link will be published as they become available.