Feeds:
Posts
Comments

Posts Tagged ‘Code Contracts’

Howdy people,

Me again with some more information of how both Code Contracts and Pex can be used together to write expressive tests (while still specifying a (partial) specification of the code). In the course of this article wel’ll also cover Assertions and Assumptions. In order to point out only the necessary topics, let’s introduce a new (very basic) sample project, and let’s perform the following steps:

  • Create a console application called MusicStore
  • Create the class Artist (as of Figure 1)
  • Create the class Album (as of Figure 2)
  • Enable Code Contracts checking (both static and runtime, as of figure 3)

clip_image002

Figure 1: The Artist class of the MusicStore project.

clip_image004

Figure 2: The Album class of the MusicStore project.

clip_image006

Figure 3: Enabling both Runtime Checking (Full), and Static Checking

Important: Do not forget to also check the Implicit Non-Null Obligations, as of Figure 3

The only critical point for CC should be the SellAlbum method of the Artist class. Why? Simply, because there we might have a parameter of type Album that could be NULL. And the Static Checker gives us the correct hints to it, as expected:

clip_image008

Figure 4: Expected CC’s Static Checker suggestion and warning.

So we have one suggestion to put a precondition, and an effective warning that we might be passing a parameter that could be NULL. This was predictable.

Running Pex over the method SellAlbum reveals the following results (If you need a starting point for Pex, please look at my article First steps with PEX: Automated White box Testing for .NET)

clip_image010

Figure 5: Pex results for 3 test cases, one providing the album parameter = NULL. Please note also the typical Pex exploration results’ table showing one column per parameter (in this case only album ).

What happens if we put an assertion to this critical parameter? Let’s simply add one, as shown in Figure 6:

clip_image012

Figure 6: Adding an assertion using a call to the static method Contract.Assert(bool condition) of the CC framework.

It makes sense to assert a number of AlbumsSold higher or equal to 1 (after 1 album has been sold), right? Does putting an assertion have an impact on Pex? Of course! Let’s run it again to see how:

clip_image014

Figure 7: Effects on Pex of using Code Contracts’ Assertions. Pex clearly identifies this as an assertion failure, hence letting the generated test case fail. Line 2 (highlighted the additionally created Pex test for the Code Contracts assertion).

So far, so good. Let’s look at Figure 6 again. We can also put such an assertion for the album object. This clearly makes sense – since selling an album should increase the album’s TimesSold count. Let’s do this in Figure 8:

clip_image016

Figure 8: Added another assertion for the album.TimesSold property.

And immediately, let’s look at the Static Checker warnings and the generated Pex test cases (Figures 9 and 10):

clip_image018

Figure 9: One more unproven assert warning for our newly added Assertion in the SellAlbum method. This was expected. Let’s run Pex again!

clip_image020

Figure 10: Line 3 shows the newly generated (and failed) test case of Pex. Again, this was expected.

Great coverage – but What About the Meaning?

This is a good question. Is this still an expressive test? Let’s recap the meaning. We could have an Album -type parameter passed, which could be theoretically NULL. Would it make any sense to then test its property TimesSold? I am sure, we can agree on that this would not be the case.

So, what we need, is the possibility to prevent Pex from generating test cases in such a case, hence producing only meaningful tests. And who is going to provide us with such a capability?

Code Contracts’ Assumptions

Important: Assumptions only work when the Full contract option is checked in the Code Contracts pane (under our project’s properties)

Figure 11 gives a brief example of how to put such an assumption into our code of the SellAlbum method.

clip_image022

Figure 11: Creating assumptions.

Figure 11 needs some explanations:

The first three assumptions simply protect us from getting the current object, the passed album, or the passed album’s artist as NULL. Makes sense, so far. The following two assumptions ensure that this.AlbumsSold and album.TimesSold both are non-negative values.

(Note also that now we put our assertions INSIDE the artist comparison’s block – makes sense, since we do not need to assert when there happened no increase of AlbumsSold and TimesSold properties).

What do We Expect?

Well, we pretty much thought at everything, didn’t we? So we expect Pex to not issue any errors or failures again. A simple re-run of Pex will show us the result, as can be seen in Figure 12.

clip_image024

Figure 12: Unexpected error on line 3, a failed assertion.

An unexpected failure? How could that happen? Let’s look at what the parameters looked like in the case of failure:

image

Did you see it? AlbumsSold is equal to int.MaxValue ! I guess, I do not need to explain what happens, if you try to increase an integer (in SellAlbum ) which is already equal to its maximum value! But why did that happen?

Simply put, this is one of the boundary test cases we explained in First steps with PEX: Automated White box Testing for .NET article. Pex guesses from the type of variables which are the boundary values (and also intermediate values).

To summarize shortly & sweetly today’s lecture:

Code Contracts & Pex: meaningful, expressive tests

(by preventing test case generation for assumed parameter values)

Let’s stop here today. There are more interesting topics regarding Code Contracts and Pex, and I am quite sure this will keep us busy for another while!

Enjoy playing around with Pex and Code Contracts, and see you next time!

Best regards,

Martin

Advertisements

Read Full Post »

Howdy all,

Here comes another post about Code Contracts. Remember my post First Steps with Code Contracts?

Let’s just recall which class we have been working on last time:

   1: namespace Vehicles

   2: {

   3:     class Car : IVehicle

   4:     {

   5:         string name;

   6:         int speed;

   7:

   8:         public Car(string name, int speed)

   9:         {

  10:             this.name = name.ToUpper();

  11:             this.speed = speed;

  12:         }

  13:

  14:         void IVehicle.Drive(int speed)

  15:         {

  16:             Console.WriteLine("Car " + name +

  17:             " is driving at a speed of " + speed);

  18:         }

  19:

  20:         public bool IsFasterThan(Car c2)

  21:         {

  22:             Console.WriteLine(name.ToUpper() +

  23:             " is faster than "

  24:             + c2.name.ToUpper());

  25:             if (this.speed > c2.speed)

  26:                 return true;

  27:             else return false;

  28:         }

  29:

  30:         [ContractInvariantMethod]

  31:         void ObjectInvariant()

  32:         {

  33:           Contract.Invariant(name != null);

  34:         }

  35:     }

  36: }

Snippet 1: The Car class from the First Steps with Code Contracts example.

After completing all the steps from that example, in the end we should have ended up with at least one warning generated by Code Contracts:

Code Contracts: Possibly calling a method on a null reference ‘c2.name’

with respect to line 24.

Now, if we review the usage of Object Invariants (First Steps with Code Contracts), we would see immediately that the purpose of Objects invariants is to provide us a mechanism to perform the checking in ObjectInvariant() in all instances (and instances of subclasses) of Car.

It seems there are no assumptions generated for the Objects Invariants of objects of the same type passed as a parameter (at least not yet, maybe it’ll come).

The workaround:

In order to avoid the warning, we can do 2 things:

  • Assumption:Contract.Assume(!String.IsNullOrEmpty(name)) or
  • Postcondition: Create a property w/ getter postcondition ensuring the result is not null

That should about do the trick!

Enjoy and see you next time!

Martin

Read Full Post »

Howdy,

The Code Contracts User Manual holds (besides detailed information about Code Contracts’ usage, advantages and drawbacks) a few nice lists of Code Snippets that ship with the Code Contracts and will ease your life. Find below the list of available Code Snippets for the C# language, as exactly taken from the User Manual (January 12th, 2010):

cr Contract.Requires(…);
ce Contract.Ensures(…);
ci Contract.Invariant(…);
crr Contract.Result<…>()
co Contract.OldValue(…)
cim [ContractInvariantMethod]

private ObjectInvariant()

{

Contract.Invariant(…);

}

crn Contract.Requires(… != null);
cen Contract.Ensures(Contracts.Result<…>() != null);
crsn Contract.Requires( !String.IsNullOrEmpty(…) );
cesn Contract.Ensures( !String.IsNullOrEmpty(Contracts.Result<string>()) );
cca Contract.Assert(…);
cam Contract.Assume(…);
cre Contract.Requires<E>(…);
cren Contract.Requires<ArgumentNullException>(… != null);
cresn Contract.Requires<ArgumentException>( !String.IsNullOrEmpty(…) );
cintf expands to an interface template and associated contract class

If you plan to use Code Contracts effectively, this list comes in very handy. I hope it’s of use for you. In the Code Contracts User Manual, you can find a similar list also for Visual Basic.

Best regards,

Martin

Read Full Post »

Hello all,

This time we’ll do a quick exploration of how we can apply Code Contracts to interfaces. As you know from our post First Steps with Code Contracts, the preconditions and postconditions (Contract.Requires and Contract.Ensures calls, respectively) must be placed inside a method body.

Therefore, when defining an interface, we run into a problem: We do not have method bodies there. Of course we could put such calls inside each effective implementation of the interface methods. Clearly, this is not what we want, since

  • We do not want to replicate code in x classes that implement our interface and
  • Future implementations of our interface would contain the conditions we need

Luckily, the Code Contracts provide us with a powerful mechanism that allows us to define a class which implements that interface and which will do the necessary checks.

The Contract Class

Let’s see how this is done, right? For this example, please recall our example from the First Steps with Code Contracts introductory article.

 

   1: namespace Vehicles

   2: {

   3:     interface IVehicle

   4:     {

   5:         void Drive(Int32 speed);        

   6:     }

   7: }

Snippet 1: The IVehicle interface

Also do recall that we did not define any pre- or postconditions for our interface (how could we? – there is no method body).

This is exactly the place, where we will put a so called Contract Class, that will implement our interface. Every time the interface is called, the conditions put into our Contract Class will be injected. This holds for every implementation of our interface.

We basically need two things:

1. A class that implements our interface IVehicle that is marked as Contract Class via an attribute:

 

   1: [ContractClassFor(typeof(IVehicle))]

   2: public class IVehicleContract : IVehicle

   3: {

   4: }

Snippet 2: Contract Class implementing the interface we want to fulfil requirements

2. Another class that links up our interface to the ContractClass

   1: [ContractClass(typeof(IVehicleContract))]

   2: public partial interface IVehicle

   3: {

   4: }

Snippet 3: The link between the interface and our Contract Class

Hint: Don’t worry: You do not have to implement these two classes from scratch: The Code Contracts come with a bunch of predefined snippets that can be executed right away. The following snippet will do the trick for generating the Contract Classes for an interface:

 

cintf ->(TAB – TAB)

The next step is to implement the interface for IVehicleContract.

clip_image002

Figure 1: Explicitly implementing the interface IVehicle for the IVehicleContract class.

The result is shown in Snippet 4:

   1: [ContractClassFor(typeof(IVehicle))]

   2: public class IVehicleContract : IVehicle

   3: {

   4:     void IVehicle.Drive(int speed)

   5:     {

   6:         throw new NotImplementedException();

   7:     }

   8: }

As a next step, we can implement our conditions in the method body of IVehicle.Drive method in IVehicleContract, like shown in Snippet 5:

   1: [ContractClassFor(typeof(IVehicle))]

   2: public class IVehicleContract : IVehicle

   3: {

   4:     void IVehicle.Drive(int speed)

   5:     {

   6:         Contract.Requires(speed >= 0);

   7:     }

   8: }

Snippet 5: precondition in interface method implementation.

What does this mean now? Well, for every implementation of the interface IVehicle , the code precondition will be injected. In other words:

 

The condition we define in the Contract Class must hold for all implementations of the interface.

 

That was it already (for this time)! It is as simple to use as it seems.

 

Enjoy and stay tuned for the next time!

Best regards,

Martin

Read Full Post »

Hello all,

Today we are going to talk about another exciting project from the Microsoft Research Labs: Code Contracts. It is a Design-By-Contract (DbC) system, that enables us as developers to formulate the expected behaviour of our code by directly putting it into the code.

The main tools of applying Code Contracts are:

  • Static checking (checks contracts at compile time)
  • Runtime checking (checks contracts at runtime)
  • Automated documentation generation (keeps code and docs in sync)

Prerequisites

Before we get started using Code Contracts. I used the following environment for carrying out the tests with Code Contracts:

  • Windows 7
  • Visual Studio 2010 Beta 2 Ultimate*
  • Code Contracts Tools*

Important: I used Visual Studio 2010 Beta 2, because it contains the .NET framework 4, which already includes the Code Contracts framework. You could also use them with VS2008, if you installed the .NET framework 4. The Code Contract Tools need to be downloaded separately. I highly recommend them, since they will add a new pane to your VS2010 which in turn lets you set various options, like enabling the static checker directly from the UI.

1.1 The Strengths of Code Contracts

Elevating assertions to the API level. At this point, the specification of code is not only somewhere deeply hidden in the method, but immediately visible to the caller (if, for example, a Contract is not fulfilled). On the other side, a caller now can know perfectly what to expect from a method.

1.2 Code Contracts for Methods

First, we are going to show how to implement Code Contracts on the method level.

We’ll start with the creation of a test project that will serve our purposes of showing Code Contracts’ capabilities:

image

Figure 1: Add a new console application and name it Vehicles

As a next step, we create a class and an interface, namely Car and IVehicle. Implement them as follows in the snippets 1 and 2. Leave the automatically generated Program class – we’ll need it later for running our examples.

   1: using System;

   2: using System.Collections.Generic;

   3: using System.Linq;

   4: using System.Text;

   5:

   6: namespace Vehicles

   7: {

   8:     interface IVehicle

   9:     {

  10:         void Drive(Int32 speed);

  11:     }

  12: }

Snippet 1: Interface IVehicle, defining one method signature

   1: namespace Vehicles

   2: {

   3:     class Car : IVehicle

   4:     {

   5:         string name;

   6:         int speed;

   7:

   8:         public Car(string name, int speed)

   9:         {

  10:             this.name = name.ToUpper();

  11:             this.speed = speed;

  12:         }

  13:

  14:         void IVehicle.Drive(int speed)

  15:         {

  16:             Console.WriteLine("Car " + name +

  17:             " is driving at a speed of " + speed);

  18:         }

  19:

  20:         public bool IsFasterThan(Car c2)

  21:         {

  22:             Console.WriteLine(name.ToUpper() +

  23:             " is faster than "

  24:             + c2.name.ToUpper());

  25:

  26:             if (this.speed > c2.speed)

  27:                 return true;

  28:             else return false;

  29:         }

  30:     }

  31: }

Snippet 2: Class Car implementing IVehicle.

So far, so good, right? Nothing special there, and the code has got very simple “functionality”. A car that can drive, alright. And check whether it is faster than another car. Compiling the project reveals a succeeding build which at first sight contains no errors.

Before we take further steps, let’s activate the Static Checking feature of Code Contracts. In order to enable this, just right-click the project Vehicles -> Properties.

The last pane on the bottom of the Properties’ window is called Code Contracts. Go for it.

clip_image004

Figure 2: The Code Contracts’ configuration in Properties. Then proceed with Figure 3.

image

Figure 3: Enable static contract checking and the checking of implicit non-null obligations.

Compile again, and in the warning sections, we’ll receive a bunch of warnings generated by Code Contracts:

image

Figure 4: Warning list, generated by Code Contracts.

Those messages are suggestions of how we should change our code in order to be (more likely to be) safe from exceptions.

The warnings, line by line:

1-2: Tell us that we should add a pre-condition in order to be sure from NullReferenceExceptions when accessing the property name (1) or passing a parameter that could be possible equal to null (2). The cool thing is: Code Contracts even provide us with the correct code in order to achieve this.

3-5: These are the actual warnings, containing possible failures.

Preconditions

A precondition is simply added by using the following method:

Contract.Requires(condition)

When debugging, we can step over such a call and verify that it is actually executed. The call is made in the method body, at any desired position. Usually it is placed at the beginning.

Postconditions

A postcondition is simply added by using the following method:

Contract.Ensures(condition)

When debugging, we cannot step over such a call (to be precise: not at the position where we put it in the code), since it is not actually executed in the method body, but only afterwards. Once we stepped over the complete method, we arrive at the Contract.Ensures call. The following snippet show how pre- and postconditions can be applied to the methods of our class Car:

   1: using System;

   2: using System.Collections.Generic;

   3: using System.Linq;

   4: using System.Text;

   5: using System.Diagnostics.Contracts;

   6:

   7: namespace Vehicles

   8: {

   9:     class Car : IVehicle

  10:     {

  11:         string name;

  12:         int speed;

  13:

  14:         public Car(string name, int speed)

  15:         {

  16:             Contract.Requires(name != null);

  17:             this.name = name.ToUpper();

  18:             this.speed = speed;

  19:         }

  20:

  21:         void IVehicle.Drive(int speed)

  22:         {

  23:             Console.WriteLine("Car " + name +

  24:             "is driving at a speed of " + speed);

  25:         }

  26:

  27:         public bool IsFasterThan(Car c2)

  28:         {

  29:             Contract.Requires(c2 != null);

  30:             Console.WriteLine(name.ToUpper() +

  31:             " is faster than " +

  32:             c2.name.ToUpper());

  33:

  34:             if (this.speed > c2.speed)

  35:                 return true;

  36:             else return false;

  37:         }

  38:     }

  39: }

Snippet 3: The Car class, using Code Contracts’ preconditions

After we added the Contract.Requires calls in IsFasterThan and in the Car ctor, we receive only 2 warnings from Code Contracts. Just compile to verify that.

Why still two warnings? We added preconditions to check that!

The reason: Only our method IsFasterThan in this particular class, Car, requires name to be non-null. But we could have for example a subclass inheriting from Car, which does not perform the same check. Hence, we need to take care for that. And in fact, Code Contracts provides us the necessary means in order to ensure that no object deriving from Car, can have name which is null:

   1: [ContractInvariantMethod]

   2: void ObjectInvariant()

   3: {

   4:     Contract.Invariant(name != null);

   5: }

Snippet 4: Object invariants

Calling again reveals that the warning concerning the name variable of class Car has gone. Good! It means, we are safe from accessing a null value – variable, and all other programmers subclassing our Car are safe, too!

This is it for now! Next time we’ll see how to deal with Code Contracts and interfaces.

Enjoy playing with Code Contracts and see you soon!

Best regards,

Martin

Read Full Post »