Code contract inheritance and the Liskov principle

With code contracts you may easily define pre-conditions, post-conditions and variants to check the parameters, results and internal state of an object instance. But what will happen if you create a new class based on a class which contains code contracts? Within this article you will see how contract inheritance can be used and whether this concept is corresponding to the Liskov principle.

 
Example application

The example application is based on the application developed during the previous article of this series. The application contains a Person class with Name and Age properties. Furthermore the class contains an Initialize method to set up all properties.

 
Contract inheritance

The example class contains the Initialize method with two pre-conditions and two post-conditions.

public class Person
{
    private string _name;
    private int _age;

    public string Name { get { return _name; } }
    public int Age { get { return _age; } }

    public virtual void Initialize(string name, int age)
    {
        Contract.Requires(name != null);
        Contract.Requires(age >= 0);
        Contract.Ensures(Name == name);
        Contract.Ensures(Age == age);

        //init properties
        _name = name;
        _age = age;
    }
}

 

Based on this class a new class customer should be created. A customer contains all data of a person and an additional number.

public class Customer : Person
{
    private int _customerNumber;
    private static int _customerNumberCounter = 0;

    public int CustomerNumber { get { return _customerNumber; } }

    public override void Initialize(            
        string name, 
        int age)
    {
        //init
        base.Initialize(name, age);

        _customerNumberCounter++;
        _customerNumber = _customerNumberCounter;
    }
}

 

If you now create a new customer instance, the code contracts of the person class will be checked. These contracts where inherited by the customer class. They will also be checked if base.Initialize is not called.

class Program
{
    static void Main(string[] args)
    {
        Customer myCustomer = new Customer();

        myCustomer.Initialize("John Doe", -1);

        Console.ReadKey();
    }
}

 

If you execute this code an error message will be shown because the following contract is violated: Contract.Requires(age >= 0);

 
Add new contracts

Of course, you may add new contracts to the new class. These contracts will extend the existing ones. For example you may add a new pre-condition and a new post-condition.

public class Customer : Person
{
    private int _customerNumber;
    private static int _customerNumberCounter = 0;

    public int CustomerNumber { get { return _customerNumber; } }

    public override void Initialize(
        string name,
        int age)
    {
        Contract.Requires(age >= 18);
        Contract.Ensures(CustomerNumber > 0);

        //init
        base.Initialize(name, age);

        _customerNumberCounter++;
        _customerNumber = _customerNumberCounter;
    }
}

 

Now the existing code contracts and the new conditions will be checked.

But wait, maybe you already see an issue with this code. Will it fulfill the Liskov principle?

 
The Liskov principle

In summary, the Liskov principle states that it should always be safe to use a subclass in any place where the parent class is expected. This sounds like a fairly easy to implement concept, but in practice this concept is often violated. And unfortunately there is no easy way to detect such a violation and so I don’t know an object-oriented language compiler which will check for this issue. But maybe code contracts can help in this situation.

To fulfill the Liskov principle, you need to adhere to a simple rule: The domain of a method can’t be shrunk in a subclass. Therefore it is not allowed to add additional pre-conditions in a derived class. If you add pre-conditions, you will restrict the range of possible values being accepted for a method. In this case the derived class will have another behavior than the base class, which violates the Liskov principle.

But what is with post-conditions and invariants? According to the Liskov principle it is allowed to add post-conditions and invariants, because this will not change the behavior of a class.

So let us think again about the previous example.

public class Customer : Person
{
    private int _customerNumber;
    private static int _customerNumberCounter = 0;

    public int CustomerNumber { get { return _customerNumber; } }

    public override void Initialize(
        string name,
        int age)
    {
        Contract.Requires(age >= 18);
        Contract.Ensures(CustomerNumber > 0);

        //init
        base.Initialize(name, age);

        _customerNumberCounter++;
        _customerNumber = _customerNumberCounter;
    }
}

 

With respect to Liskov principle it should not be allowed to add the pre-condition but it should be allowed to add the post-condition. And now you can see the power of code contracts. In contrast to the compiler, they will recognize this violation of the Liskov principle. The following warning is shown:

Method ‚…‘ overrides ‚…‘, thus cannot add Requires.

 

Therefore we have to change the code and remove the additional pre-condition to fulfill the Liskov principle. The following code shows the adapted class.

public class Customer : Person
{
    private int _customerNumber;
    private static int _customerNumberCounter = 0;

    public int CustomerNumber { get { return _customerNumber; } }

    public override void Initialize(
        string name,
        int age)
    {
        Contract.Ensures(CustomerNumber > 0);

        //init
        base.Initialize(name, age);

        _customerNumberCounter++;
        _customerNumber = _customerNumberCounter;
    }
}

 
Summary

Code contracts will support inheritance and therefore they easily support the object oriented concept of base classes and derivate classes. Furthermore it is recognized whether the contract inheritance fulfills the Liskov principle. This may prevent implementation errors in connection with class inheritance.

Werbung
Dieser Beitrag wurde unter .NET, C# veröffentlicht. Setze ein Lesezeichen auf den Permalink.

Kommentar verfassen

Trage deine Daten unten ein oder klicke ein Icon um dich einzuloggen:

WordPress.com-Logo

Du kommentierst mit deinem WordPress.com-Konto. Abmelden /  Ändern )

Facebook-Foto

Du kommentierst mit deinem Facebook-Konto. Abmelden /  Ändern )

Verbinde mit %s