Interface Inheritance and Contracts

In the Code Contracts library, which kindly provides contract programming capabilities on the .NET platform, calls for static methods of the Contract class are used to set preconditions and postconditions. On the one hand, this is good, since an attribute-based alternative implementation would be too limited. On the other hand, it adds certain difficulties when it comes to interface contracts or abstract methods, which, by their nature, do not contain any code, and therefore they simply have no reason to call methods.

This is solved using two attributes: ContractClassAttribute , which hangs on the interface or an abstract class, and ContractClassForAttribute - which hangs on the contract itself.

/// <summary> /// Custom collection interface /// </summary> [ContractClass(typeof(CollectionContract))] public interface ICollection { void Add(string s); int Count { get; } bool Contains(string s); } /// <summary> /// Contract class for <see cref="ICollection"/>. /// </summary> [ContractClassFor(typeof(ICollection))] internal abstract class CollectionContract : ICollection { public void Add(string s) { Contract.Ensures(Count >= Contract.OldValue(Count)); Contract.Ensures(Contains(s)); } public int Count { get { Contract.Ensures(Contract.Result<int>() >= 0); return default(int); } } [Pure] public bool Contains(string s) { return default(bool); } } 

The benefits of this ICollection interface seem doubtful, but with their help we will be able to see all the necessary possibilities and limitations of contracts, with respect to the inheritance of interfaces. This example focuses on the two members of the CollectionContract class: the Add method and the Count property, which define the preconditions / postconditions of the corresponding methods.
')
Now, if some class implements our ICollection interface and violates the postcondition, we will see it at runtime as an exception (with a certain CONTRACT_FULL symbol), and also, possibly, during static analysis of the Static Checker code:

 internal class CustomCollection : ICollection { private readonly List<string> _backingList = new List<string>(); public void Add(string s) { // Ok, we're crazy enough to violate precondition // of ICollection interface if (Contains(s)) _backingList.Remove(s); else _backingList.Add(s); } public int Count { get { // We should add some hints to static checker to eliminate a warning Contract.Ensures(Contract.Result<int>() == _backingList.Count); return _backingList.Count; } } public bool Contains(string s) { return _backingList.Contains(s); } } 

In this case, this is exactly what happens: Static Checker determines that in some cases the postcondition of the Add method fails (when adding an existing element, we delete itJ). But if we do not believe him, we can see a breach of contract during the execution.

 [Test] public void TestAddTwiceAddsTwoElements() { var collection = new CustomCollection(); int oldCount = collection.Count; collection.Add(""); collection.Add(""); Assert.That(collection.Count, Is.EqualTo(oldCount + 2)); } 

This test will not crash when calling Assert. That , and earlier, when trying to call the Add method again, with the following exception: System.Diagnostics.Contracts .__ ContractsRuntime + ContractException: Postcondition failed: Count> = Contract.OldValue (Count)

NOTE
Static analysis is one of the most interesting features of "contract programming", but now we can safely say that this thing in the Code Contracts library is not yet ready for real projects. Firstly, the compilation time can increase by an order of magnitude (!), Secondly, it is necessary not to jump around with a tambourine around him so that he understands what is happening, but even in this case he will be little able to help in difficult cases. Even in such a simple example, as with the CustomCollection class, we had to add the postcondition to the Count property manually, because without it, the static analyzer did not understand what was happening and gave a lot of warnings. All other advantages of contracts, such as declarativeness, documentation, formalization of relations, etc. remain, but they will work at runtime (for example, in conjunction with unit tests), and not at compile time.

Weakening of precondition and postcondition strengthening

Contracts allow you to formalize relationships not only between classes and their clients, but also between classes and their heirs. The preconditions of the virtual method will tell the client what to do to call this method, and the postcondition what the method will do in return; Moreover, the client code can count on the execution of this contract, regardless of what the dynamic type of the object it works with will be. This is what the principle of replacing Liskov says, which we discussed last time and to which we will return.

However, the principle of substitution does not prohibit heirs from making changes to the semantics of the method, unless it “breaks” the assumptions of customers. Thus, the precondition of a method redefined in the successor may be less stringent to the calling code (it may contain a weaker precondition), and the postcondition may be more stringent — the inheritor method may produce a more “accurate” result. To translate from Russian into Russian, let's consider a simple example:

 class Base { public virtual object Foo(string s) { Contract.Requires(!string.IsNullOrEmpty(s)); Contract.Ensures(Contract.Result<object>() != null); return new object(); } } class Derived : Base { public override object Foo(string s) { // Now we're requiring empty string Contract.Requires(s != null); // And returning only strings Contract.Ensures(Contract.Result<object>() is string); return s; } } 

In this example, the inheritor method requires less: the empty string is now a valid value; and gives a more “accurate” result: it returns not just the object , but the type string (although this is guaranteed not by the compiler, but by the Static Checker).

NOTE
A typical example of post-condition enhancement is the ability of derived classes to return a more specific type. This feature is called covariance on the return type and is available in languages ​​such as C ++ or Java. If C # supported this feature, it would be possible to change the signature of the method Derived.Foo and return a string , not an object . Another example of weakening preconditions and enhancing postconditions is the covariance and contravariance of delegates and interfaces, available from the 4th version of the C # language. You can read more about the “strictness” of the conditions in the article Design by Contract. On the correctness of software , and on contracts and inheritance - in the article Design by contract. Inheritance .

The developers of Code Contracts considered the possibility of weakening the postconditions to be meaningless, so we have no such possibility. The above Derived class code is compiled, but the precondition of the Derived method . Foo is not weakened, which means that when a blank line is passed, the precondition will be violated. However, unlike the preconditions, with the post-conditions we are almost all in order. Postconditions (by the way, like class invariants) are "summed up", which really allows us to guarantee more. (If you change the body of the method Derived . Foo so that in some cases it returns an int rather than a string , then this violation will be detected by Static Checker and will also be checked at runtime.)

Postconditions and interfaces

Now let's move from base classes to interfaces. In the first section, we looked at the ICollection interface, the post -condition of which was “not decreasing” the number of elements in the collection. This postcondition is derived from the ICollection of T interface contract from the BCL. After installing Code Contracts, we have at our disposal not only the possibility of creating contracts for our own classes, but also the possibility of using contracts of standard classes from the BCL.

But before proceeding to the analysis of contracts of standard interfaces, let's try to create our own hierarchy of interfaces, and play around with the postconditions of the Add method.

 [ContractClass(typeof(ListContract))] public interface IList : ICollection { } [ContractClassFor(typeof(IList))] internal abstract class ListContract : IList { public void Add(string s) { // Lets create stronger postcondition than ICollection.Add Contract.Ensures(Count == Contract.OldValue(Count) + 1); } //   Count   Contains   } 

This IList interface adds not only post-conditions, but also a bunch of other interesting things, but in this case it does not matter. Now add a class that implements the IList interface, which violates the post-condition of the interface:

 public class CustomList : IList { private readonly List<string> _backingList = new List<string>(); public void Add(string s) { // IList postcondition is Count = OldCount + 1, // we're violating it _backingList.Add(s); _backingList.Add(s); } public int Count { get { return _backingList.Count; } } public bool Contains(string s) { return _backingList.Contains(s); } } 

We clearly violate the post-condition of the Add method of the IList interface, since it increases the number of elements not by one, but immediately by 2. However, the sad thing is that neither the static analyzer, nor even the rewriter does not react to the increased post-conditions at the interfaces. Now, as a matter of fact, this possibility is not supported by the Code Contract library (and the developers consider this a feature, not a bug, see the details here ). So at the moment we can strengthen the post-conditions of virtual methods, we can strengthen the post-condition in a class that implements some interface, but we cannot strengthen the post-conditions in the heirs of interfaces !

The trouble with this point is the following: first, the only way to find out about the existence of more strictly interface postconditions is to manually search for the contract code (recall that neither the Static Checker nor the rewriter adds information about the postcondition of the successor to the result code); secondly, this example is not artificial, this problem can be encountered using standard interfaces of the BCL collections.

Contracts ICollection of T and IList of T

If you rummage properly in the mscorlib assembly . Contracts . dll , which appears after installing Code Contracts, then you can find a lot of interesting things about the contracts of the standard .NET Framework classes and collection contracts, in particular. Here are the contracts for the basic methods of the ICollection of T and IList of T interfaces:

 // From mscorlib.Contracts.dll [ContractClassFor(typeof(ICollection<>))] internal abstract class ICollectionContract<T> : ICollection<T>, IEnumerable<T>, IEnumerable { public void Add([MarshalAs(UnmanagedType.Error)] T item) { Contract.Ensures(this.Count >= Contract.OldValue<int>(this.Count), "this.Count >= Contract.OldValue(this.Count)"); } public void Clear() { Contract.Ensures(this.Count == 0, "this.Count == 0"); } public int Count { get { int num = 0; Contract.Ensures(Contract.Result<int>() >= 0, "Contract.Result<int>() >= 0"); return num; } } } // From mscorlib.Contracts.dll [ContractClassFor(typeof (IList<>))] internal abstract class IListContract<T> : IList<T>, ICollection<T>, IEnumerable<T>, IEnumerable { void ICollection<T>.Add([MarshalAs(UnmanagedType.Error)] T item) { Contract.Ensures(this.Count == (Contract.OldValue<int>(this.Count) + 1), "Count == Contract.OldValue(Count) + 1"); } public int Count { get { int num = 0; return num; } } } 

NOTE
Contracts for different versions of the .NET Framework are located in different places, contracts for the 4th version of the framework, for example, are located in the following path: “% PROGRAMS% \ Microsoft \ Contracts \ Contracts \ .NETFramework \ v.4.0 \”. Assemblies with contracts are called as follows: OriginalAssemblyName.Contracts.dll: mscorlib.Contracts.dll, System.Contracts.dll, System.Xml.Contracts.dll.

As we can see, the post-condition of the list is really stronger and it requires that when calling the Add method a new element appears in the list, and only one. The difference in the postconditions of the two interfaces is due to the fact that not all BCL collections add a new element when calling the Add method ( HashSet and SortedSet do not add an element if it is already present in the collection); however, all lists add only one new item. This problem is solved by adding an explicit postcondition to a specific collection class ( List of T or, in our case, the DoubleList class), but in this case the main feature of interface contracts is lost: the ability to specify the behavior of the class family.

Conclusion

Not all developers are comfortable thinking about interface contracts or abstract methods, because in .NET they do not contain any information about the intended behavior. But if you look at it from the other side, the importance of contracts specifically for such methods is much higher. In the case of a specific method, we can look at its implementation and define explicit or implicit preconditions and postconditions. But to define an interface contract, we can repel only scanty and informal documentation or analyze all implementations of this interface to determine the “common” denominator of behavior that should not be violated according to the substitution principle.

Additional links

1. ContractsAndInheritance project on GitHub . Contains all the examples of this article with tests and comments.
   
2. Bertrand Meyer. Object-oriented design of software systems
   
3. Design by contract. Inheritance