August 24, 2009 at 09:49Contract programming in the .NET Framework 4
Faced with the problem of changing work and the desire to work as a developer in a good office, I realized that I lacked knowledge in the field of architecture, design, OOP, and other things not specific to the platform or language. Sources of information, in addition to personal experience, are standard - books and the Internet.
By that time, Fowler's books on refactoring and the GoF book had been read. These books gave me a lot and were very useful, but I wanted something more fundamental about OOP. Searching the forums, I found several books that interested me:
Bertrand Meyer, “Object-Oriented Design of Software Systems”
Grady Butch, Object-Oriented Analysis and Design by
Barbara Liskov. Using abstractions and specifications in software development
Unfortunately, I did not find the latter in electronic form, and in paper I do not even know where to look. From the presence in the store at that time was only a book by Meyer, I took it.
I liked the book, streamlined and explained a lot, although some nuances remained. The translation, as a whole, is literate, it was made by people who are aware of technology and terminology. Unfortunately, I did not find the year of writing the text, but as I understood it, around the mid-90s. This largely explains why the author so diligently argues that OOP is better than other approaches that were popular at that time. I didn’t really like some points. First, a lot of attention is paid to some negativity about functional programming. The second, in general, the whole book, as it seemed to me, was written in the style of "There are two opinions, one mine, the other wrong." The author created the Eiffel language, which was based on the principles described in the book, all controversial and boundary decisions are interpreted in favor of the author, accompanied by crushing comments of another option. Sometimes it becomes incomprehensible how the Java and C # languages with such “huge flaws” became popular. Although, we must admit that generics were very expected in both Java and .Net.
A red thread runs through the whole book is the idea of contract programming. Each subprogram (method) may have a precondition and a postcondition. The precondition sets the properties that must be executed each time the program is called; the postcondition determines the properties guaranteed by the program upon its completion. Preconditions and postconditions describe the properties of individual programs. But class instances also have global properties. They are called class invariants, and they define deeper semantic properties and integrity constraints that characterize the class. The invariant is added to the precondition and postcondition. Contract programming is a great way to document code, debug, and eliminate unnecessary checks. For example, if the postcondition says that the method returns a non-negative number, then there is no need to check the number for non-negativity when extracting the square root. All this leads to increased reliability, quality and speed of development.
Unfortunately, .Net developers (were) deprived of the opportunity to use this approach in their work. You can of course use Debug.Assert, but that’s not quite right. Assert allows you to set conditions for a specific section of code, although they can be used instead of preconditions and postconditions. But there are still class invariants that are set for all class methods and, possibly, descendants.
The contract system consists of four main parts. The first part is the library. Contracts are encoded using the static method call of the Contract class (System.Diagnostics.Contracts namespace) from the mscorlib.dll assembly. Contracts are declarative in nature, and these static calls at the beginning of your methods can be considered as part of the method signature. They are methods, not attributes, because attributes are very limited, but these concepts are close.
The second part is binary rewriter, ccrewrite.exe. This tool modifies the MSIL instructions and validates the contract. This tool provides an opportunity to verify the execution of contracts to help with debugging the code. Without it, contracts are just documentation and are not included in the compiled code.
The third part is a static verification tool, cccheck.exe, which analyzes the code without executing it and tries to prove that all contracts are completed.
The fourth part is ccrefgen.exe, which creates a separate assembly containing only the contract.
There are three main forms of preconditions, two of which are based on the Requires method of the Contract class. Both approaches have overloaded options that allow you to include a message in case of breach of contract.
This method is an easy way to specify what is required when entering the method. The Requires form makes it possible to throw an exception in case of contract violation.
The third form of preconditions is to use the if-then-throw construct to test the parameters.
This approach has its advantages in that it is performed every time it starts. But the contract system has more features (tools, inheritance, etc.). To turn this construct into a contract, you need to add a call to the Contract.EndContractBlock () method
The if-then-throw construct may occur several times in the method code, but only if the construct starts the method and after it the Contract.EndContractBlock () method is called, this code will be a contract.
Postconditions.
There are two options for postconditions: the first guarantees a normal return, the second guarantees something when throwing the specified exception.
The second option (made for illustration)
If you pass zero to this method, the contract will be violated.
Postcondition is checked when exiting the method
The invariant is encoded using the Invariant method.
They are declared in a single method of the class that contains only invariants and is marked with the ContractInvariantMethod attribute. By tradition, this method is called ObjectInvariant and mark protected so that you cannot call this method explicitly from someone else's code.
There are several possible scenarios for using contracts for debugging. One of them is the use of static analysis and contract analysis tools. The second option is a run-time check. To get the most out of it, you need to know what happened when the contract was violated. Two stages can be distinguished here: notification and reaction.
If the contract is violated, an event occurs.
Remember that this is a prerelease, and something may change for the final release.
You can use this event for logging.
If you use a test framework, you can do something like this (example for the Visual Studio framework)
Inheritance
Many in the comments find similarities with Debug.Assert and unit testing. In addition to the originally various goals, a significant difference is inheritance. Contracts are inherited!
Example, console application,
and programm.cs code
In this example, the contract will be violated. The amplification-easing conditions are also taken into account. According to Meyer, the heir has the right to weaken the precondition (accept more options) and strengthen the postcondition - to further limit the return value.
This is natural given dynamic binding and polymorphism.
This article is based on an article (free translation with abbreviations) Code Contracts by Melitta Andersen
Related links.
By that time, Fowler's books on refactoring and the GoF book had been read. These books gave me a lot and were very useful, but I wanted something more fundamental about OOP. Searching the forums, I found several books that interested me:
Bertrand Meyer, “Object-Oriented Design of Software Systems”
Grady Butch, Object-Oriented Analysis and Design by
Barbara Liskov. Using abstractions and specifications in software development
Unfortunately, I did not find the latter in electronic form, and in paper I do not even know where to look. From the presence in the store at that time was only a book by Meyer, I took it.
A bit about the book.
I liked the book, streamlined and explained a lot, although some nuances remained. The translation, as a whole, is literate, it was made by people who are aware of technology and terminology. Unfortunately, I did not find the year of writing the text, but as I understood it, around the mid-90s. This largely explains why the author so diligently argues that OOP is better than other approaches that were popular at that time. I didn’t really like some points. First, a lot of attention is paid to some negativity about functional programming. The second, in general, the whole book, as it seemed to me, was written in the style of "There are two opinions, one mine, the other wrong." The author created the Eiffel language, which was based on the principles described in the book, all controversial and boundary decisions are interpreted in favor of the author, accompanied by crushing comments of another option. Sometimes it becomes incomprehensible how the Java and C # languages with such “huge flaws” became popular. Although, we must admit that generics were very expected in both Java and .Net.
Programming by contract.
A red thread runs through the whole book is the idea of contract programming. Each subprogram (method) may have a precondition and a postcondition. The precondition sets the properties that must be executed each time the program is called; the postcondition determines the properties guaranteed by the program upon its completion. Preconditions and postconditions describe the properties of individual programs. But class instances also have global properties. They are called class invariants, and they define deeper semantic properties and integrity constraints that characterize the class. The invariant is added to the precondition and postcondition. Contract programming is a great way to document code, debug, and eliminate unnecessary checks. For example, if the postcondition says that the method returns a non-negative number, then there is no need to check the number for non-negativity when extracting the square root. All this leads to increased reliability, quality and speed of development.
Unfortunately, .Net developers (were) deprived of the opportunity to use this approach in their work. You can of course use Debug.Assert, but that’s not quite right. Assert allows you to set conditions for a specific section of code, although they can be used instead of preconditions and postconditions. But there are still class invariants that are set for all class methods and, possibly, descendants.
Parts of the contract system in .Net framework 4.0.
The contract system consists of four main parts. The first part is the library. Contracts are encoded using the static method call of the Contract class (System.Diagnostics.Contracts namespace) from the mscorlib.dll assembly. Contracts are declarative in nature, and these static calls at the beginning of your methods can be considered as part of the method signature. They are methods, not attributes, because attributes are very limited, but these concepts are close.
The second part is binary rewriter, ccrewrite.exe. This tool modifies the MSIL instructions and validates the contract. This tool provides an opportunity to verify the execution of contracts to help with debugging the code. Without it, contracts are just documentation and are not included in the compiled code.
The third part is a static verification tool, cccheck.exe, which analyzes the code without executing it and tries to prove that all contracts are completed.
The fourth part is ccrefgen.exe, which creates a separate assembly containing only the contract.
Library of contracts. Precondition.
There are three main forms of preconditions, two of which are based on the Requires method of the Contract class. Both approaches have overloaded options that allow you to include a message in case of breach of contract.
public Boolean TryAddItemToBill(Item item)
{
Contract.Requires(item != null);
Contract.Requires(item.Price >= 0);
}
* This source code was highlighted with Source Code Highlighter. This method is an easy way to specify what is required when entering the method. The Requires form makes it possible to throw an exception in case of contract violation.
The third form of preconditions is to use the if-then-throw construct to test the parameters.
public Boolean ExampleMethod(String parameter)
{
if (parameter == null)
throw new ArgumentNullException("parameter must be non-null");
}
* This source code was highlighted with Source Code Highlighter.This approach has its advantages in that it is performed every time it starts. But the contract system has more features (tools, inheritance, etc.). To turn this construct into a contract, you need to add a call to the Contract.EndContractBlock () method
public Boolean ExampleMethod(String parameter)
{
if (parameter == null)
throw new ArgumentNullException("parameter must be non-null");
// tells tools the if-check is a contract
Contract.EndContractBlock();
}
* This source code was highlighted with Source Code Highlighter.The if-then-throw construct may occur several times in the method code, but only if the construct starts the method and after it the Contract.EndContractBlock () method is called, this code will be a contract.
Postconditions.
There are two options for postconditions: the first guarantees a normal return, the second guarantees something when throwing the specified exception.
public Boolean TryAddItemToBill(Item item)
{
Contract.Ensures(TotalCost >= Contract.OldValue(TotalCost));
Contract.Ensures(ItemsOnBill.Contains(item) || (Contract.Result() == false));
Contract.EnsuresOnThrow(TotalCost == Contract.OldValue(TotalCost))
}
* This source code was highlighted with Source Code Highlighter. The second option (made for illustration)
public int Foo(int arg)
{
Contract.EnsuresOnThrow(false);
int i = 5 / arg;
return i;
}
* This source code was highlighted with Source Code Highlighter. If you pass zero to this method, the contract will be violated.
Postcondition is checked when exiting the method
public class ExampleClass
{
public Int32 myValue;
public Int32 Sum(Int32 value)
{
Contract.Ensures(Contract.OldValue(this.myValue) == this.myValue);
myValue += value; //это нарушение контракта и будет отловлено
return myValue;
}
}
* This source code was highlighted with Source Code Highlighter.Invariant
The invariant is encoded using the Invariant method.
public static void Invariant(bool condition);
public static void Invariant(bool condition, String userMessage);
* This source code was highlighted with Source Code Highlighter.They are declared in a single method of the class that contains only invariants and is marked with the ContractInvariantMethod attribute. By tradition, this method is called ObjectInvariant and mark protected so that you cannot call this method explicitly from someone else's code.
[ContractInvariantMethod]
protected void ObjectInvariant()
{
Contract.Invariant(TotalCost >= 0);
}
* This source code was highlighted with Source Code Highlighter.Debugging with contracts.
There are several possible scenarios for using contracts for debugging. One of them is the use of static analysis and contract analysis tools. The second option is a run-time check. To get the most out of it, you need to know what happened when the contract was violated. Two stages can be distinguished here: notification and reaction.
If the contract is violated, an event occurs.
public sealed class ContractFailedEventArgs : EventArgs
{
public String Message { get; }
public String Condition { get; }
public ContractFailureKind FailureKind { get; }
public Exception OriginalException { get; }
public Boolean Handled { get; }
public Boolean Unwind { get; }
public void SetHandled();
public void SetUnwind();
public ContractFailedEventArgs(ContractFailureKind failureKind,
String message, String condition,
Exception originalException);
}
* This source code was highlighted with Source Code Highlighter.Remember that this is a prerelease, and something may change for the final release.
You can use this event for logging.
If you use a test framework, you can do something like this (example for the Visual Studio framework)
[AssemblyInitialize]
public static void AssemblyInitialize(TestContext testContext)
{
Contract.ContractFailed += (sender, eventArgs) =>
{
eventArgs.SetHandled();
eventArgs.SetUnwind(); // cause code to abort after event
Assert.Fail(eventArgs.Message); // report as test failure
};
}
* This source code was highlighted with Source Code Highlighter.UPD
Inheritance
Many in the comments find similarities with Debug.Assert and unit testing. In addition to the originally various goals, a significant difference is inheritance. Contracts are inherited!
Example, console application,
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace ConsoleApplication1
{
class ClassWithContract
{
int intNotNegativeField;
[ContractInvariantMethod]
protected virtual void ObjectInvariant()
{
Contract.Invariant(this.intNotNegativeField >= 0);
}
public virtual int intNotNegativeProperty
{
get
{
return this.intNotNegativeField;
}
set
{
this.intNotNegativeField = value;
}
}
public ClassWithContract()
{
}
}
class InheritFromClassWithContract : ClassWithContract
{
}
}
* This source code was highlighted with Source Code Highlighter.and programm.cs code
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
namespace ConsoleApplication1
{
class Program
{
static void Main(string[] args)
{
InheritFromClassWithContract myObject = new InheritFromClassWithContract();
myObject.intNotNegativeProperty = -3;
}
}
}
* This source code was highlighted with Source Code Highlighter.In this example, the contract will be violated. The amplification-easing conditions are also taken into account. According to Meyer, the heir has the right to weaken the precondition (accept more options) and strengthen the postcondition - to further limit the return value.
This is natural given dynamic binding and polymorphism.
This article is based on an article (free translation with abbreviations) Code Contracts by Melitta Andersen
Related links.
- msdn.microsoft.com/en-us/library/system.diagnostics.contracts ( VS.100 ) .aspx
- msdn.microsoft.com/en-us/devlabs/dd491992.aspx
- msdn.microsoft.com/en-us/magazine/ee236408 (en-us) .aspx
- habrahabr.ru/blogs/crazydev/38612
- en.wikipedia.org/wiki/Design_by_contract
- www.eiffel.com/developers/design_by_contract.html