Motley says: "Contracts do me no good at run-time"

  • Article

Summary

 

Motley: I am not going to take time to specify my API contracts if there are no tools to help validate them

 

Maven: Languages like Spec# and Eiffel have Design By Contract semantics built-in and can greatly improve the reliability of your software

______________________________

 

[Context:  A continuing conversation between Maven and Motley about contracts - this time about tools]

 

Motley: I can see how thinking about interface contracts - including preconditions, postconditions, and class invariants - can help drive unit test creation. But, I am definitely not going through the effort of writing all this stuff down. I'll just use it to help my thinking.

 

Maven: Well, it definitely helps thinking, but there can be reasons to formally specify - write down - the contract around your APIs.

 

Motley: For what benefit?

 

Maven: Some languages, like Eiffel, have had what are called "design by contract" constructs for years to help developers build higher quality software. These constructs are also making their way into more modern languages like C#, which you use every day.

 

Motley: I don't remember seeing like this in the C# language. Are you high on something?

 

Maven: Actually, Microsoft is doing a bunch of work here, but it is still mostly research at this point. The technology is called Spec#, and it adds Design By Contract constructs as an addition to the C# language.

 

Motley: Ahhhh… research = vaporware.

 

Maven: Well, not quite Mr. Pessimist. There actually IS a Visual Studio add-in that you can play with today. I'll give you the link later.

 

Motley: I noticed you used the word "play" above. Not ready for prime time?

 

Maven: You are very good at reading into things. That's right - I would not use it in production code at the moment, but if I was a betting man, I would think that Microsoft will include the constructs in the language in the future.

 

Motley: Ok, I am curious enough - how does it work?

 

Maven: Assuming you understand preconditions, postconditions, and class invariants as we discussed previously, you already understand the concepts behind Spec#. The native Spec# implementation makes some enhancements to the C# compiler such that it understands some new keywords. I'll talk about the ones most related to design by contract and bold them below. Here is an example:

 

public class Employee

{

private string employeeName;

 

public void CreateEmployee(string name)

requires name != null && name.Length > 0 otherwise ArgumentException;

{

this.employeeName = name;

}

 

public string ToString()

invariant employeeName ! = null;

ensures value.Length > 0;

{

return "Employee: " + this.employeeName;

}

}

 

Maven: The code above uses the following keywords that are added to C# by Spec#:

  • requires: specifies a precondition; the name input parameter must not be null and must not be blank. If this condition is violated, an ArgumentException is thrown automatically.
  • invariant: When this routine executes the conditions must be true before and after; employeeName must be non-null.
  • ensures: specifies a postcondition; the return value of the method must contain a non-empty string

 

Motley: So how exactly is the contract checked? I would hope I am not doing all this work just to validate by hand.

 

Maven: Definitely not. The compiler inserts some inline prolog and epilog code into the compiled binary to check the conditions and throw exceptions to the caller if they are not satisfied. There is also a code analysis tool called "Boogie" that will check all of your code statically to make sure that all callers abide by the contracts.

 

Motley: Sounds interesting, but until it's ready for production code, I am not buying stock.

 

Maven: The important part is to understand the concepts and realize that design by contract is going to be more important moving forward. Plus, as we talked about previously, you can still use the concept to drive your unit tests. For now, C# still contains exception handling that you can use to validate things like preconditions, and debug assertions to validate invariants - definitely better than nothing. There's also a lot more that Spec# can do, but we'll save that for another time if you're interested.

______________________________

 

Maven's Pointer: Design By Contract (DBC) has been around for a while, but is an underused technique to develop very reliable software. The developer mentality changes a bit when developing an API with a contract - you typically first think about and specify the contract before any implementation whatsoever. Then, regardless of what the implementation is, the contract typically stays the same.

 

Maven's Resources:  Spec# from Microsoft Research, The Spec# Programming System: An Overview, Spec# Wiki, Design By Contract Overview in Eiffel