LA.NET [EN]

Design by ContractArchive

Apr 07

Protected: The OnDeserializingAttribute – part II

Posted in C#, Design by Contract, WCF       Comments Off on Protected: The OnDeserializingAttribute – part II

This content is password protected. To view it please enter your password below:

Apr 22

Code Contracts…are cool again!

Posted in Design by Contract       Comments Off on Code Contracts…are cool again!

Why, you ask?

Simply because now they’re usable from within any version of Visual Studio (though you’ll only have static checking if you’re using VSTS). I’m not sure on how I missed that announcement (ok, I missed it because I got really “depressed” after the initial requisites for using it and never looked back!), but now I’m really excited and will start migrating all my existing code for using this new platform…

Feb 25

Code contract is out

Posted in C#, Design by Contract       Comments Off on Code contract is out

Check the announcement here and the site is here.

Nov 19

If you look closely at your bin folder, you’ll see that besides getting your project’s assembly, you’ll also have another assembly with the your_Assembly_name.Contracts.dll name. This assembly is known as the contract reference assembly and it only has the public “interface” of the types defined on your assembly and their respective contracts.

Why do we need this assembly? It is used during the rewriting process to inherit contracts across assemblies. According to the docs, they’re also used for static analyses to discover contracts on methods from other referenced assemblies when you’re performing static validation on a project.

So, this kind of assembly is really important and you should generate them and redistribute them with your assemblies. If you’re using VS, then don’t worry because they will be automatically generated for you. If you’re not using VS or the code contract msbuild task to build your project, then you’ll need to use the command line asmmeta.exe to generate it.

And I guess that this means that the intro series on code contracts is over. It’s time to pick another subject…suggestions?

Nov 18

Code contracts: the missing methods

Posted in C#, Design by Contract       Comments Off on Code contracts: the missing methods

In the last posts, I’ve been talking extensively about Code Contracts. If you’re a reader of this blog, you know that I’m hooked on it. I’ve just been reviewing the previous posts and I’ve noticed that I didn’t mention the Assert and Assume methods. Both are used for testing state and  assumptions on a specific point of the program. As you might expect, they follow the same syntax as the other methods that have been presented in the past.

Interestingly, both methods let you use members with less visibility than the method where you’re using them. At runtime, both have the same behavior and will only delegate to the Assert method of the runtime rewriter when you define the CONTRACTS_FULL constant on your code. btw, by default the predefined rewriter will call the Debug.Assert method.

The Assume method is interesting, especially when you think about the static analysis step. All the assumptions that you add (ie, every Assume method call) will be added to the “known facts” list maintained by the static validation tool and will be used by it to check other existing contracts  on that scope. What this means is that you should use Assume for giving the validation tool more info about some facts which you know to be true at runtime, but that won’t be inferred by the static analysis tool.

The best way to test this concepts is to run a small example and start adding Assert and Assume method calls. Unfortunately, I didn’t had the necessary time for building such a sample,so you’ll have to do it yourself….

Nov 12

Code Contracts and runtime rewriting

Posted in C#, Design by Contract       Comments Off on Code Contracts and runtime rewriting

Today we’re going to keep looking at Code Contracts. Until now, I’ve been concentrating essentially in presenting its use and mentioning how great it is to have static analysis (ie, have something that goes through your code at compile time and detects several places which might breaking existing contracts). Today it’s time to take a look at the advantages associated with its use at runtime.

You’ll get runtime “support” (lets call it this, ok?) whenever you define the CONTRACTS_FULL constant on your code. The easiest way to achieve this is to go to your VS project property window and check the Perform Runtime Contract Checking checkbox (that is near the top of the window). When you do that, you’ll get some interesting things going on on your build. For starters, your assembly will be rewritten. In practice, this means that:

  • postconditions are moved to the end of the method;
  • method return values are replaced by CodeContracts.Result occurences (more on this on the next paragraphs);
  • pre-state values are replaced with CodeContacts.OldValue occurrences;
  • contracts are enforced in inheritance scenarios (hurray!).

All this work is done automatically by the ccrewrite tool. If you just go ahead and build a project with Code Contracts runtime support enabled, you’ll see that you’ll get assertions at runtime when one of your contracts is not respected. If you want, you can change that behavior. For instance, lets say that I wanted to get an exception instead of getting the Debug.Assert followed by the Environment.FailFast method calls that are used by default…

Since I’m lazy, I’ll just create a new Exception derived class. If this was production code, I’d probably be creating an exception type for each  kind of contract verification (ie,one for preconditions,another for postconditions, etc). Since this is just demo, I’ll probably be able to get away with only one class (ok, I’m really being lazy here! DO check the guidelines before writing your exceptions):

public class DbCException: Exception    {
        public DbCException(String message)
            :base(message)
        {}
}

What we need now is a way to throw these exceptions whenever a contract is broken. According to the docs, we need to add a class which has several static methods (one for each “type” of contract):

namespace Test {
public class CustomRewriter {
        public static void Requires(Boolean condition, String message)
        {
            if (!condition) throw new DbCException(message);
        }

        public static void Ensures(Boolean condition, String message) {
            if (!condition) throw new DbCException(message);
        }

        public static void Assert(Boolean condition, String message) {
            if (!condition) throw new DbCException(message);
        }

        public static void Assume(Boolean condition, String message) {
            if (!condition) throw new DbCException(message);
        }

        public static void Invariant(Boolean condition, String message) {
            if (!condition) throw new DbCException(message);
        }
}
}

And that’s it. Now, you only need to pass the necessary information for the ccrewrite tool to use these classes instead of the default ones. If you’re using VS, just go to the project’s property window and write the name of the assembly that has the previous classes and the complete name of the class that has the static methods.

Suppose that the CustomRewriter class was on an assembly called anotherassembly. In that case, you should put anotherassembly.dll on the Assembly textbox and Test.CustomRewriter on the Class textbox (do notice that I had to add the dll extension for it to work – not sure if this will remain like this on future versions). Oh, and I almost was forgetting to mention that you need to put that custom assembly on the same folder as the assembly that is being rewritten.

Before ending the post, there’s still time for a quick analysis of the rewriting process. To show you what happens, lets reuse the example presented in the post about quantifiers. Lets focus on the OnPeople method. Originally, it looked like this:

public PersonSearcher OnPeople(Person[] people) {
  CodeContract.Requires(CodeContract.ForAll(0, people.Length, pos => people[pos] != null));
  CodeContract.Ensures(_people != null);
  _people = people;
  return this;
}

After the ccrewrite tool ends its work, it will look like this:

public PersonSearcher OnPeople(Person[] people)
{
    __copy+<>c__DisplayClass1 CS$<>8__locals2 = new __copy+<>c__DisplayClass1();
    CS$<>8__locals2.people = people;
    CustomRewriter.Requires(CodeContract.ForAll(0, CS$<>8__locals2.people.Length, new Predicate<int>(CS$<>8__locals2.<OnPeople>b__0)), "CodeContract.ForAll(0, people.Length, pos => people[pos] != null)");
    this._people = people;
    PersonSearcher CS$1$0000 = this;
    PersonSearcher Contract.Result<PersonSearcher>() = CS$1$0000;
    CustomRewriter.Ensures(this._people != null, "_people != null");
    return Contract.Result<PersonSearcher>();
}

If you go back to the previous list on what happens when rewriting happens, things should start to make sense (please don’t concentrate on the lambdas rewritings done by the compiler; they’re not important in this scenario).

CodeContract.Requires is replaced by a call to the “custom” static CustomRewriter.Requires method. Another thing you’ll notice is that the return value is replaced by a Contract.Result local variable (in order to ensure that the postcondition is correctly run, the rewriting process will introduce a field called Contract.Result so that that you can use it in your postconditions – this wasn’t needed in the previous example though). Finally, the Ensures postcondition verification is moved from the top to the bottom of the method. I’ll leave it to you the verification associated with the use of the OldValues method call.

And that’s all for today. We’re getting near the end of this series on Code Contracts. There are still a couple of things  I’d like to mention, so stay tuned if you want to read my ramblings on it.

Nov 09

Code Contracts also supports are quantifiers (with several limitations, as we’ll see). This means that you can check a predicate against elements in a collection or interval. You can use the ForAll method for running a predicate over several elements maintained on an collection or interval. The Exists method will let you apply a predicate and see if there is at least one item in the  specified collection or interval that validates that predicate.

Consider these two classes:

public class Person {
        public String Name { get; set; }
}
public class PersonSearcher {
        private String _name;
        private IEnumerable<Person> _people;
        public PersonSearcher SearchFor(String name) {
            _name = name;
            return this;
        }
        public PersonSearcher OnPeople(IEnumerable<Person> people) {
            _people = people;
            return this;
        }
        public Person Get() {
            return _people.SingleOrDefault( p => String.CompareOrdinal(p.Name, _name) == 0);
        }
}

There’s a simple Person class and a PersonSearcher class which checks if a specific person in on a collection of Persons. Suppose that one of the things we’d like to make sure is that all the items on the people collection that are passed as a parameter are non null. This is easily done by using the ForAll method:

public PersonSearcher OnPeople(IEnumerable<Person> people) {
    CodeContract.Requires(
                         CodeContract.ForAll(people, p => p != null));
    _people = people;
    return this;
}

And now you do get verification on all the instances of people passed as an argument. For instance, if you try to run this code, you’ll get a Debug.Assert at runtime:~

var people = new[]
                             {
                                 null,
                                 new Person {Name = "Luis"},
                                 new Person {Name = "John"},
                                 new Person {Name = "Charles"}
                             };
new PersonSearcher().SearchFor("Luis").OnPeople(people);

If the method received an array, you could also use the other overload method:

public PersonSearcher OnPeople(Person[] people) {
  CodeContract.Requires(
   CodeContract.ForAll(0, people.Length, pos => people[pos] != null));
CodeContract.Ensures(_people != null);
_people = people;
return this;
}

The Exists method is really similar to the ForAll method,so I won’t be writing any example to show its usage. On the next post,we’ll start looking at runtime behavior. Keep tuned!

Nov 08

Code Contracts and compatibility with existing code

Posted in C#, Design by Contract       Comments Off on Code Contracts and compatibility with existing code

Before using Code Contracts, you’ll probably already written several lines of validation code for testing requirements on your methods. I’ll keep using the Person class to illustrate some code that you might have before using the Code Contracts library. So, in the past, you might have something like this:

public class Person {
        private String _firstName;
        private String _lastName;
        public String FirstName {
            get { return _firstName; }
        }
        public String LastName {
            get { return _lastName; }
        }
        public void ChangeName(string firstName, string lastName) {
            if( firstName == null )
                    throw new ArgumentNullException("firstName");
            if( lastName== null )
                    throw new ArgumentNullException("lastName");
            _firstName = firstName;
            _lastName = lastName;
        }
}

Now, the first thing you could do is port your code and replace those if-then-throw statements with calls to CodeContracts.Requires method. That might be quite a bit of work! The good news is that if your code is located at the beginning of the method’s body and is similar to the previous example (ie, it’s in the form of if-then-throw), then you can simply add one line of code to the bottom of those tests and you’ll get all the benefits associated with the direct usage of Code Contracts’s methods. Here’s the changes needed for the previous method:

public void ChangeName(string firstName, string lastName) {
    if( firstName == null )
          throw new ArgumentNullException("firstName");
    if( lastName== null )
          throw new ArgumentNullException("lastName");
    CodeContract.EndContractBlock();
    _firstName = firstName;
    _lastName = lastName;
}

Now, if you try writing the following snippet:

var p = new Person();
p.ChangeName(null, null);

You’ll get a warning at compile time. And that’s it for today. More about this on future posts. Keep tuned.

Nov 07

Adding Code Contracts to your interfaces

Posted in C#, Design by Contract       Comments Off on Adding Code Contracts to your interfaces

[Update: I’ve changed the code so that the contract class implements the interface explicitly. This is required for getting static analysis. One more thing: the first release of the project has a bug and  even if you implement the interface explicitly, you won’t get static analysis.]

One of the interest things Code Contracts lets you do is define additional contracts on your interfaces. To achieve this, you need to add a “dumb” class which implements that interface and add the required contracts to the body of the methods. To illustrate the necessary work, lets start by creating a new interface called IPerson:

public interface IPerson {
   String FirstName { get; }
   String LastName { get; }
   void ChangeName(String firstName, String lastName);
}

One of the things I’d like to guarantee is that the method ChangeName will only receive valid names. As we’ve seen in a previous post, that is easily achievable by using the CodeContract.Requires method. Since you cannot define a body on C# interface methods, you’ll need to create a new class which implements the interface and has the restrictions you want to apply:

public class PersonContract:IPerson { 
  string IPerson.FirstName {
            get { return CodeContract.Result<String>(); }
  } 
  string IPerson.LastName {
            get { return CodeContract.Result<String>(); }
  } 
  void IPerson.ChangeName(string firstName, string lastName) {
            CodeContract.Requires(firstName != null);
            CodeContract.Requires(lastName != null);
}
}

It’s important to notice that the contract class must implement the interface explicitly. Since I don’t care about the value returned by the methods on that class, I’ll reuse the values returned by CodeContract.Result<T> method (notice that you can return any valid value from the implementation of the interface in the “contract class”). Now, we need to identity the PersonContract class as the one that defines the contract we want to enforce on our interface. This is achieved with the ContractClassAttribute and ContractClassForAttribute attributes. The first is applied to the interface and the second is applied to the class:

[ContractClass(typeof(PersonContract))]
public interface IPerson    {
   //previous code
}

[ContractClassFor(typeof(IPerson))]
public class PersonContract:IPerson    {
   //previous code
}

And now, you can build the “domain” classes and you’ll automatically inherit the contracts “attached” to the interface. For instance, here’s a valid implementation  for the previous interface:

public class Person:IPerson {
       private String _firstName;
       private String _lastName; 
       public String FirstName {
           get { return _firstName; }
       } 
       public String LastName {
           get { return _lastName; }
       } 
       public void ChangeName(string firstName,string lastName)
       {
           _firstName = firstName;
           _lastName = lastName;
       }
}

Notice how we didn’t add any sort of validation to the class…Simply great,right? On the next post, I’ll keep talking about this great library for applying design by contract on your .NET code. Keep tuned!

Nov 06

More on Code Contracts: out parameters and field access on preconditions

Posted in C#, Design by Contract       Comments Off on More on Code Contracts: out parameters and field access on preconditions

In this post we’ll keep looking at how Code Contracts can really help you improve your code. Today, we’ll see how one can use fields and out parameters in contracts. Lets start with fields. Ok, the title is a little misleading…you can use fields in your contract. But what happens when you need to define a contract on an private field from a public method? Well, lets think about this for a minute…your clients must check for values so that they won’t break the contract. If you’re specifying a contract on a private field, then how will a client validate the contract before invoking the method? That’s why there’s a restriction on the visibility of the members you can use in a contract…

In the previous scenario, you could always wrap your field on a property and use the property from within the precondition. However, there may be some cases where calling the property isn’t really desired (for instance, your property might perform some additional tasks which aren’t really necessary when you’re testing the contract). In those cases, and if you have your field is wrapped by a property which is at least as visible as the place where you specifying the contract, then you can use the ContractPublicPropertyNameAttribute and use the field on your contract. Here’s another really simple example:

public class Person
    {
        public Person(String name)
        {
            Name = name;
        }
        [ContractPublicPropertyName("Name")]
        private String _name;
        public String Name {
             get{ /*suppose you have more code here*/return _name;}
             set{ _name = value;}
       }

        public void ChangeName(String name)
        {
            CodeContract.Requires( _name == null);
            Name = name;
        }
    }

If you compile the previous example, you’ll see that you won’t get any errors or warnings and you’ll be able to use a private field on a contract defined on a public method.

Before ending the post, there’s still time to see how you can use out parameters on your contracts. Honestly,I don’t remember the last time I’ve used an out or ref parameter (without being in a interop scenario). Anyway,if you need it, you can use the CodeContract.ValueAtReturn<T> method for using that parameter on a contract. And that’s all for today. More about this framework tomorrow

Nov 06

Code Contracts: don’t use the overloads that receive a string

Posted in C#, Design by Contract       Comments Off on Code Contracts: don’t use the overloads that receive a string

In my first post about Code Contracts I’ve mentioned that in my machine static analysis wasn’t picking up those evident scenarios where the code was breaking the predefined contracts. Today I’ve got the confirmation on the PEX forum (which, btw, is the place where you should post your questions regarding this framework while we don’t have a discussion place for this framework).

Nov 06

More on code contracts: checking return values and old values

Posted in C#, Design by Contract       Comments Off on More on code contracts: checking return values and old values

Today I’ll keep writing about the new Code Contracts framework and we’ll see how we can use the write contracts that validate method return values and “old” values. Lets start with method return values…

As you might expect, you’re able to refer to return values on your postconditions. To show you the kind of thing you’ll be writing, we will start by changing the class we presented yesterday and we’ll add a BirthDate property to it:

class Student{

private DateTime _birthDate;
public DateTime BirthDate {
            get { return _birthDate; }
            set {
                CodeContract.Requires(value> new DateTime(1900, 1, 1));
                _birthDate = value;
            }
  } 
}

Now, we can calculate the age by adding a new method called CalculateAge to this class. This probably is a good way to implement it:

class Student{
  public Int32 CalculateAge()  {
            var currentDate = DateTime.Now;
            var years = currentDate.Year – _birthDate.Year;
            if( currentDate.CompareTo(_birthDate.AddYears(years)) < 0 )
            {
                years–;
            }
            return years;
   }
}

Ok, so one of the things we can do is make sure that we return a valid age. Just to be sure, we can say that the age of a person must always be bigger than 0, so we’ll go ahead and add that condition:

public Int32 CalculateAge()  {
        CodeContract.Ensures( CodeContract.Result<Int32>() > 0 );
        //previous code
}

The CodeContract.Result<T> method is generic and can only be called inside the Ensures method. T should be replaced by the return type of the method.

Besides specifying the contract for the return value, you can also use another special method: CodeContract.OldValue<T>. This method expects a parameter of type T and there are several restrictions which apply to the values that can be passed to it. For instance, the return value (CodeContract.Result<T>) cannot be used on the expression passed to that parameter. You can’t also use out parameters either! The docs contain full list with these rules, so I won’t be putting them here. Instead,I’ll show how you can apply these method in your code.

One of the things you can do is guarantee that you’ll only update the value of the field _birthDate if the new date is different than the existing one. You can also specify this with a contract.Here’s an example (ok,sorry for the lame example, but I’m a little but tired today:)):

public DateTime BirthDate {
   get { return _birthDate; }
   set {
     CodeContract.Requires(value > new DateTime(1900, 1, 1));
     CodeContract.Ensures(
            CodeContract.OldValue(_birthDate) != _birthDate);
      _birthDate = value;
   }
}

Ok, this should be enough for showing you how you can use the OldValue method. So, if you try to write this code:

var st = new Student(2);
st.BirthDate = new DateTime(1976, 6, 27);
//more code here…
st.BirthDate = new DateTime(1976, 6, 27);

You’ll surely get an assert at runtime (on the next posts, we’ll see how easy it is to replace the assert with, say, an exception – which is something I really prefer). And that is it for today, As I said earlier, the examples might not have been the best, but I think that they were enough for illustrating the usage of return methods and old values in your contracts. On the next post, we’ll keep looking at this framework and see how you can use non-public fields and out parameters in your contracts. Keep tuned!

Nov 05

Yesterday I was really excited after finding out that we’ll finally have a library for performing Design By Contract verifications on our code. Ok, the runtime validations could already be simulated by writing some code (I’ve already written several helpers classes in my current applications), but the truth is that the Code Contracts library adds static verification and will enable you to catch several errors during compilation. I believe this is more than enough for you to be interested in this new library, right?

Ok, so lets start with a basic scenario which will let me illustrate the usage of the existing static methods available on the CodeContract class (attention: do notice that this class will be renamed into Contract on the final release): lets suppose we have a simple class called student which looks like this:

public class Student
{
        private String _firstName = "";
        private String _lastName = ""; 
        public Student(Int32 studentId)
        {
            StudentId = studentId;
        } 
        public Int32 StudentId { get; private set; } 
        public String FirstName { get { return _firstName; } } 
        public String LastName { get { return _lastName; } } 
        public void ChangeName(String firstName, String lastName)
        {
            _firstName = firstName;
            _lastName = lastName;
        } 
}

One of the things you’ll want to apply to your methods are preconditions for checking parameter values. For instance, lets assume that only positive integers are valid for student ids. So, if you try to run the following code:

var std = new Student( –1 );

You should get an error at runtime. If you use a precondition, you’ll also get a compile warning (yes, you’ve read it correctly: *compile* warning). Here’s what you need to do to achieve that:

public Student(Int32 studentId) {
   CodeContract.Requires(studentId > 0);
   StudentId = studentId;

Btw, the CodeContract class is defined on the System.Diagnostics.Contracts namespace. Besides simple conditions, you can also,for example,call pure methods. A pure method is annotated with the PureAttribute and when you do that, you’re actually saying that the method doesn’t produce any side effects (using methods might give you false positives too!).

Besides your own methods, you can also access property getters, operators and several methods whose qualified name begins with System.String, System.IO.Path, System.Type and, of course, CodeContract methods. Do notice that whenever you access another member, you’ll have to make sure that that member has at least the same visibility as the method where you’re adding your contracts.

One more note: when you install the code contract bits, your projects will get an additional tab on the property page which you’ll have to configure for having static and runtime analysis. Not setting the checkboxes means that you won’t have either of those validations.

Besides checking  values, you can also give some guarantees regarding the state of your object after your method ends. For instance, in the previous example you can say that when the constructor does its job, you’ll always have a positive ID. Here’s how you can do that:

public Student(Int32 studentId) {
  CodeContract.Requires(studentId > 0 );
  CodeContract.Ensures(StudentId > 0);
  StudentId = studentId;
}

You can also ensure state when you get an exception. You do this by calling EnsuresOnThrow generic method. When you do this, you’re saying that even if you get an exception, the predicate you specify should be met.

You can also use invariants. Invariants define conditions under which an object is in a good state. By adding an invariant, you’re defining a group of predicates that will always be run after all your public method calls. An invariant is defined through a protected method which only contains several Ensures method calls. For instance, if we think that ensuring that the StudentId is always positive is really necessary for guaranteeing the good state of our instances of Student, then we can add a method that looks like this to our class:

[ContractInvariantMethod]
protected void ObjectInvariant() {
    CodeContract.Ensures(StudentId > 0);       
}

And now, whenever someone calls a public method of your class, the previous validation will always be performed. And that’s it for today. Tomorrow we’ll keep talking about code contracts. Keep tuned.

Nov 04

Ok, I know I’ve asked for design by contract on C# and that didn’t made it into C# 4.0. However, I’ve just discovered something even better (especially if you’re a VB programmer): we’re getting support for it on the form of a library and some msbuild tasks that are able to perform static and runtime analyses.

There’s an installation package that should work on VS 2008  but it seems like this framework will be migrating to the mscorlib.dll starting from CLR v4.0. YES!!! So, if like me, you’re still on Vista with VS 2008, just go ahead and download the installation package. Then, you can do two things:

  • Read the docs, which are installed on the MicrosoftContracts folder (inside  your program files folder);
  • Watch the PDC video for a demo of the product

Two things before you start jumping around in pure joy:

  1. you cannot use the current version of commercial software (there’s only an academic license – wtf???)
  2. it seems like there’s a bug and whenever you use one of the overloads of the static methods that receive a string, those validations won’t be picked up during the static analysis (I didn’t found anything on the docs about this, so I’m assuming it’s some sort of bug).

I’ve already written some code, so I’ll probably add a couple of posts on this topic on the next days. Stay tuned…