Contract programming in the .NET Framework 4
Faced with the problem of changing jobs 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, standard - books and the Internet.
By that time, Fowler’s books on refactoring and the GoF book were read. These books gave me a lot and were very useful, but I wanted something more fundamental about the PLO. Searching through the forums, I found several books that interested me:
Bertrand Meyer, "Object-Oriented Design of Software Systems"
Grady Booch, Object-Oriented Analysis and Design
Barbara Liskov. Using abstractions and specifications when developing programs
Unfortunately, the latter did not find it in electronic form, and I don’t even know where to look in paper form. From the presence in the store at that time there was only Meyer’s book, I took it.
')
I liked the book, ordered and explained a lot, although there were some nuances left. Translation, in general, literate, it was done 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 was about the mid-90s. This largely explains why the author so zealously proves that OOP is better than any other approaches that were popular at that time. Some moments I did not really like. First, much has been given to some negativity about functional programming. The second, in general, the whole book, it seemed to me, was written in the style of "There are two opinions, one is mine, the other is 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 devastating comments of another option. Sometimes it becomes incomprehensible how the Java and C # languages ​​with such “huge flaws” became popular. Although, it must be admitted that generics were very expected in both Java and .Net.
The idea of ​​programming on a contract runs through the whole book. Each subprogram (method) can be associated with a precondition and postcondition. The precondition sets the properties that must be executed each time the program is called; postcondition defines 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 the deeper semantic properties and integrity constraints that characterize a class. The invariant is added to the precondition and postcondition. Contract programming is a great way of documenting code, debugging, and eliminating unnecessary checks. For example, if it is written in a postcondition that the method returns a non-negative number, then there is no need to check the number for non-negativity when extracting a square root. All this leads to increased reliability, quality and speed of development.
Unfortunately, .Net developers (were) unable to use this approach in their work. You can certainly use Debug.Assert, but this is not exactly that. Assert allows you to set conditions for a specific piece of code, although they can be used instead of preconditions and postconditions. But there are class invariants that are set for all class methods and, possibly, heirs.
The contract system consists of four main parts. The first part is the library. Contracts are encoded using a call to the static methods of the Contract class (the 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 viewed 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 the binary rewriter, ccrewrite.exe. This tool modifies MSIL instructions and verifies the contract. This tool provides the ability to verify the execution of contracts to assist in debugging code. Without it, contracts are just documentation and are not included in the compiled code.
The third part is the static verification tool, cccheck.exe, which analyzes the code without executing it and tries to prove that all contracts have been completed.
The fourth part is ccrefgen.exe, which creates a separate assembly containing only a contract.
There are three main forms of preconditions, two of which are based on the Requires method of the class Contract. 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 a method. Requires form makes it possible to throw an exception if a contract is violated.
The third form of preconditions is the use of the if-then-throw construct to test the parameters.
This approach has its advantages in that it runs every time you start. But the contract system has more features (tools, inheritance, etc.). To turn this construction 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's code, but only if the construct starts the method and after it comes the call to the Contract.EndContractBlock () method will the given code be a contract.
Postconditions.
There are two postconditions: the first one guarantees a normal return, the second one guarantees something when a specified exception is thrown.
The second option (made for illustration)
When transferring this method to zero, the contract will be violated.
Postcondition checked on exit from method
The invariant is encoded using the Invariant method.
They are declared in a single class method that contains only invariants and is labeled with the ContractInvariantMethod attribute. By tradition, this method is called ObjectInvariant and is marked protected so that it is impossible to call this method explicitly from someone else's code.
There are several possible use cases for debugging contracts. One of them is to use static analysis and contract analysis tools. The second option is to check at run time. To get the most bang for your buck, you need to know what happened during a breach of contract. Two stages can be distinguished here: notification and reaction.
If the contract is broken, an event occurs.
Remember that this is a prerelease, and something can change to the final release.
You can use this event for logging.
If you are using 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 initially different goals, a significant difference is inheritance. Contracts are inherited!
An example console application
and programm.cs code
In this example, the contract will be broken. Gain-attenuation conditions are also taken into account. According to Meyer, the heir has the right to weaken the precondition (more options to take) and strengthen the postcondition - further limit the return value.
This is natural, given the dynamic binding and polymorphism.
This article is based on the article (free translation with abbreviations) Code Contracts , by Melitta Andersen
Related links.
By that time, Fowler’s books on refactoring and the GoF book were read. These books gave me a lot and were very useful, but I wanted something more fundamental about the PLO. Searching through the forums, I found several books that interested me:
Bertrand Meyer, "Object-Oriented Design of Software Systems"
Grady Booch, Object-Oriented Analysis and Design
Barbara Liskov. Using abstractions and specifications when developing programs
Unfortunately, the latter did not find it in electronic form, and I don’t even know where to look in paper form. From the presence in the store at that time there was only Meyer’s book, I took it.
')
A little about the book.
I liked the book, ordered and explained a lot, although there were some nuances left. Translation, in general, literate, it was done 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 was about the mid-90s. This largely explains why the author so zealously proves that OOP is better than any other approaches that were popular at that time. Some moments I did not really like. First, much has been given to some negativity about functional programming. The second, in general, the whole book, it seemed to me, was written in the style of "There are two opinions, one is mine, the other is 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 devastating comments of another option. Sometimes it becomes incomprehensible how the Java and C # languages ​​with such “huge flaws” became popular. Although, it must be admitted that generics were very expected in both Java and .Net.
Contract programming.
The idea of ​​programming on a contract runs through the whole book. Each subprogram (method) can be associated with a precondition and postcondition. The precondition sets the properties that must be executed each time the program is called; postcondition defines 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 the deeper semantic properties and integrity constraints that characterize a class. The invariant is added to the precondition and postcondition. Contract programming is a great way of documenting code, debugging, and eliminating unnecessary checks. For example, if it is written in a postcondition that the method returns a non-negative number, then there is no need to check the number for non-negativity when extracting a square root. All this leads to increased reliability, quality and speed of development.
Unfortunately, .Net developers (were) unable to use this approach in their work. You can certainly use Debug.Assert, but this is not exactly that. Assert allows you to set conditions for a specific piece of code, although they can be used instead of preconditions and postconditions. But there are class invariants that are set for all class methods and, possibly, heirs.
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 a call to the static methods of the Contract class (the 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 viewed 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 the binary rewriter, ccrewrite.exe. This tool modifies MSIL instructions and verifies the contract. This tool provides the ability to verify the execution of contracts to assist in debugging code. Without it, contracts are just documentation and are not included in the compiled code.
The third part is the static verification tool, cccheck.exe, which analyzes the code without executing it and tries to prove that all contracts have been completed.
The fourth part is ccrefgen.exe, which creates a separate assembly containing only a contract.
Library of contracts. Precondition.
There are three main forms of preconditions, two of which are based on the Requires method of the class Contract. Both approaches have overloaded options that allow you to include a message in case of breach of contract.
public Boolean TryAddItemToBill(Item item)<br>{<br> Contract.Requires<NullReferenceException>(item != null );<br> Contract.Requires(item.Price >= 0);<br>} <br><br> * This source code was highlighted with Source Code Highlighter .This method is an easy way to specify what is required when entering a method. Requires form makes it possible to throw an exception if a contract is violated.
The third form of preconditions is the use of the if-then-throw construct to test the parameters.
public Boolean ExampleMethod( String parameter)<br>{<br> if (parameter == null )<br> throw new ArgumentNullException( "parameter must be non-null" );<br>} <br><br> * This source code was highlighted with Source Code Highlighter .This approach has its advantages in that it runs every time you start. But the contract system has more features (tools, inheritance, etc.). To turn this construction into a contract, you need to add a call to the Contract.EndContractBlock () method
public Boolean ExampleMethod( String parameter)<br>{<br> if (parameter == null )<br> throw new ArgumentNullException( "parameter must be non-null" );<br> // tells tools the if-check is a contract <br> Contract.EndContractBlock();<br>} <br><br> * This source code was highlighted with Source Code Highlighter .The if-then-throw construct may occur several times in the method's code, but only if the construct starts the method and after it comes the call to the Contract.EndContractBlock () method will the given code be a contract.
Postconditions.
There are two postconditions: the first one guarantees a normal return, the second one guarantees something when a specified exception is thrown.
public Boolean TryAddItemToBill(Item item)<br>{<br> Contract.Ensures(TotalCost >= Contract.OldValue(TotalCost));<br> Contract.Ensures(ItemsOnBill.Contains(item) || (Contract.Result<Boolean>() == false ));<br> Contract.EnsuresOnThrow<IOException>(TotalCost == Contract.OldValue(TotalCost))<br>}<br> <br><br> * This source code was highlighted with Source Code Highlighter .The second option (made for illustration)
public int Foo( int arg)
{
Contract.EnsuresOnThrow<DivideByZeroException>( false );
int i = 5 / arg;
return i;
}
* This source code was highlighted with Source Code Highlighter .When transferring this method to zero, the contract will be violated.
Postcondition checked on exit from method
public class ExampleClass<br>{<br> public Int32 myValue;<br> public Int32 Sum( Int32 value )<br> {<br> Contract.Ensures(Contract.OldValue( this .myValue) == this .myValue);<br> myValue += value ; // <br> return myValue;<br> }<br>}<br> <br> * This source code was highlighted with Source Code Highlighter .Invariant
The invariant is encoded using the Invariant method.
public static void Invariant( bool condition);<br> public static void Invariant( bool condition, String userMessage); <br><br> * This source code was highlighted with Source Code Highlighter .They are declared in a single class method that contains only invariants and is labeled with the ContractInvariantMethod attribute. By tradition, this method is called ObjectInvariant and is marked protected so that it is impossible to call this method explicitly from someone else's code.
[ContractInvariantMethod]<br> protected void ObjectInvariant()<br>{<br> Contract.Invariant(TotalCost >= 0);<br>}<br> <br> * This source code was highlighted with Source Code Highlighter .Debugging with contracts.
There are several possible use cases for debugging contracts. One of them is to use static analysis and contract analysis tools. The second option is to check at run time. To get the most bang for your buck, you need to know what happened during a breach of contract. Two stages can be distinguished here: notification and reaction.
If the contract is broken, an event occurs.
public sealed class ContractFailedEventArgs : EventArgs <br>{<br> public String Message { get ; }<br> public String Condition { get ; }<br> public ContractFailureKind FailureKind { get ; }<br> public Exception OriginalException { get ; }<br> public Boolean Handled { get ; }<br> public Boolean Unwind { get ; }<br> public void SetHandled();<br> public void SetUnwind();<br> public ContractFailedEventArgs(ContractFailureKind failureKind,<br> String message, String condition, <br> Exception originalException);<br>} <br><br> * This source code was highlighted with Source Code Highlighter .Remember that this is a prerelease, and something can change to the final release.
You can use this event for logging.
If you are using a test framework, you can do something like this (example for the Visual Studio framework)
[AssemblyInitialize]<br> public static void AssemblyInitialize(TestContext testContext)<br>{<br> Contract.ContractFailed += (sender, eventArgs) =><br> {<br> eventArgs.SetHandled();<br> eventArgs.SetUnwind(); // cause code to abort after event <br> Assert.Fail(eventArgs.Message); // report as test failure <br> };<br>}<br> <br> * 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 initially different goals, a significant difference is inheritance. Contracts are inherited!
An 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 broken. Gain-attenuation conditions are also taken into account. According to Meyer, the heir has the right to weaken the precondition (more options to take) and strengthen the postcondition - further limit the return value.
This is natural, given the dynamic binding and polymorphism.
This article is based on the 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
Source: https://habr.com/ru/post/67813/
All Articles