Pedro Félix’s shared memory

Design by Contract meets .NET

Posted in Uncategorized by pedrofelix on November 9, 2008

At PDC 2008, Microsoft Research presented Code Contracts:

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of pre-conditions, post-conditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation. 

Design by Contract

Code Contracts are heavily influenced by “Design by Contract” (DbC), a method proposed by Bertrand Meyer to improve the correctness and reliability of programs.

The Design by Contract method is based on the concept of contracts as a way to specify the behavior of code artifacts such as methods. Its roots can be traced back to concepts such as Hoare triples.

The Design by Contract was proposed on the context of the object oriented paradigm, namely the Eiffel language and method.

Among other things, a contract defines the obligations between a method and it’s client, namely:

  • The client obligations, defined as require clauses or preconditions, are predicates over the client visible state that must be true when the method starts.
  • The methods obligations, named as ensure clauses or postconditions, are predicates that must be true when the method ends.

A contract provides a way to define the meaning of correct implementation. Loosely writing, a method implementation is correct if, for any call that satisfies the requires clauses, the ensures clauses are also satisfied at the end of its execution.

A contract also defines invariants, which are conditions that must hold for all observable states of an object lifetime.

Contracts also interact with class inheritance and method redefinition. Namely, the contract of a redefined method must be a sub-contract of the base method:

  • The redefined method must not require more than the base method.
  • The redefined method must not ensure less than the base method.

Contracts can be informally described in documentation or can be formally embedded in the code. This last option, adopted by the Eiffel language and method, has several advantages:

  • The mere need for defining a code contract forces the programmer to think more carefully about the method specifications, improving the code quality.
  • The existence of code contracts allows the automatic generation of code that detects contract violations at runtime.
  • Code contracts can also be used by static analysis tools to detect contract violations at build time.
  • Finally, code contracts can also be reflected in the automatically generated documentation.

The Eiffel language has specific language mechanisms to represent code contracts, as showed in the following example (note the require and ensure regions before and after the method’s body).

 

   1: integer_division(a,b:INTEGER):PAIR is
   2:         -- divisão inteira
   3:     require
   4:         non_negative_dividend: a>=0 
   5:         positive_divisor: b>0
   6:     local
   7:         r,q: INTEGER
   8:     do
   9:         from
  10:             r := a; q := 0
  11:         until
  12:             r < b
  13:         loop
  14:             r := r - b; q := q + 1
  15:         end
  16:         !!Result.make(q,r)
  17:     ensure
  18:         definition1: a = Result.first*b + Result.second
  19:         definition2: 0 <= Result.second and Result.second < b
  20:     end

 

Contracts and .NET

The Spec# project had the goal of introducing the Design by Contract concepts into the C# language. This project included: a set of language extensions to the C# language, a compiler and a static program verifier.

However, the adoption of the Spec# extensions by the C# language is not in the C# team plans, in spite of the great interest manifested by the developer community, and reflected in campaigns such as

                     

In my opinion, the Spec# project had two major drawbacks:

  • It required another major change to the C# language syntax.
  • It was not directly applicable to other .NET languages.

The Code Contracts project solves this problems by providing a language agnostic way to express contracts in code, as shown in the following code excerpt.

   1: public static Pair<int, int> integerDivision(int dividend, int divisor) {
   2:     CodeContract.Requires(dividend >= 0 && divisor>0); 
   3:  
   4:     CodeContract.Ensures(CodeContract.Result<Pair<int, int>>().first * divisor + CodeContract.Result<Pair<int, int>>().second == dividend);            
   5:     CodeContract.Ensures(CodeContract.Result<Pair<int, int>>().second >= 0 && CodeContract.Result<Pair<int, int>>().second < divisor);
   6:  
   7:     int quocient = 0;
   8:     int remainder = dividend;
   9:     while (remainder > divisor) {
  10:         remainder -= divisor;
  11:         quocient += 1;
  12:     }
  13:     return new Pair<int,int>(quocient, remainder);
  14: }

 

Instead of using language extensions, Code Contracts uses the following mechanisms:

  • The contract conditions are expressed via calls to static methods of the CodeContract class. The parameters to these calls are boolean expressions, defined using native language constructs. The CodeContract also contain additional special methods, such as the CodeContract.Result method, that represents the return value.
  • The invariant conditions are defined in a special method, annotated with the ContractInvariantMethodAttribute.
  • After the compilation step, a binary rewriter (ccrewrite.exe) is used to translate these static methods calls into the real runtime checks.

The code below shows the result of this last rewriting. Namely, notice that the Ensures calls where removed from the beginning of the method and inserted into the end.

   1: public static Pair<int, int> integerDivision(int dividend, int divisor)
   2: {
   3:     __RewriterMethods.RewriterRequires((dividend >= 0) && (divisor > 0), "dividend >= 0 && divisor>0");
   4:     int quocient = 0;
   5:     int remainder = dividend;
   6:     while (remainder > divisor)
   7:     {
   8:         remainder -= divisor;
   9:         quocient++;
  10:     }
  11:     Pair<int, int> CS$1$0000 = new Pair<int, int>(quocient, remainder);
  12:     Pair<int, int> Contract.Result<Pair`2<System.Int32,System.Int32>>() = CS$1$0000;
  13:     __RewriterMethods.RewriterEnsures(((Contract.Result<Pair`2<System.Int32,System.Int32>>().first * divisor) + Contract.Result<Pair`2<System.Int32,System.Int32>>().second) == dividend, "CodeContract.Result<Pair<int, int>>().first * divisor + CodeContract.Result<Pair<int, int>>().second == dividend");
  14:     __RewriterMethods.RewriterEnsures((Contract.Result<Pair`2<System.Int32,System.Int32>>().second >= 0) && (Contract.Result<Pair`2<System.Int32,System.Int32>>().second < divisor), "CodeContract.Result<Pair<int, int>>().second >= 0 && CodeContract.Result<Pair<int, int>>().second < divisor");
  15:     return Contract.Result<Pair`2<System.Int32,System.Int32>>();
  16: }
  17:  
  18:  
  19:  
  20:  

I end this post suggesting the download of the current release, available at the Code Contracts site. This release integrates rather well with Visual Studio 2008 (academic license only!). I also suggest the reading of the “Code Contracts User Manual” present in this release.

About these ads

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: