1-Spec #
2-NET Code Contracts
3-C++ Source Annotations
In this tutorial we will cover code contracts using Spec#, the code contracts library shipping with .NET. Code contracts allow one to specify the behavior of an algorithm by explicitly adhering to a well defined contract. Commonly, these contracts are in the form of pre- and post-conditions. Further, one can also specify behavioral contracts for a type in the form of a type invariant. For now you need not worry about how such contracts can be defined (we will discuss that later), however, it is important to understand some of the benefits of using code contracts, these include:
For many readers code contracts will not be a new concept, most likely you will have seen them before in texts on data structures and algorithms. However, most readers will be new to applying similar concepts to their actual codebase.In this tutorial we will cover code contracts using Spec#, the code contracts library shipping with .NET, and finish with a lo ok at VC++ source code annotations.
Spec# is a Microsoft Research project that extends the C# language so that you can easily define code contracts. In addition, Spec# also provides compile-time checks to verify certain assertions hold, e.g. that a non-null object is passed to an algorithm. In this section we will look at some of the features that the Spec# language introduced.
Pre-conditions define the properties that an algorithm requires to be satisfied in order to operate correctly; these properties are defined by the algorithm designer. For example, a pre-condition for an algorithm that takes a single list argument could be: verify that the number of items in l is greater than 0. If any of the pre-conditions are not satisfied then the algorithm should not execute, after all if it were to execute who knows what the behavior of the algorithm would be? Certainly, the algorithm designer never intended it to be used in such a manner. The behavior would be undefined which encompasses several things, amongst them - failure.For our first example we will look at how we can define a non-null constraint for an algorithm argument.
class MyType
{
// ...
void MyAlgorithm(First! first)
{
// ...
}
}In the previous code listing we simply added an ! after the argument type to define a non-null constraint, this constraint is checked at compile-time by the Spec# compiler. A simple, yet powerful extension to the C# language. When applying the same constraint to a type member we must use an object initializer for that member. The object intializer syntax is similar to that found in C++.
class MyType
{
MyMemberType! m_member;
// ...
MyType(MyMemberType! member) : m_member(member)
{
// ...
}
}Like non-null constraints, specifying pre-conditions in the Spec# language is very unobtrusive.
class MyType
{
void MyAlgorithm (First! first)
requires first.Value > 0 && first.Value < 100;
{
// ...
}
}In the previous example we make use of the requires keyword introduced by Spec# to define a pre-condition. If the pre-condition is not satisfied then by default a RequiresViolationException will be thrown, we can override the default exception type by using another Spec# keyword - otherwise.
class MyType
{
void MyAlgorithm (First! first)
requires first.Value > 0 && first.Value < 100;
{
// ...
}
}Post-conditions are used to ensure that certain properties will be met upon completion of an algorithm. For example, for an algorithm that increments its integer argument i, one could specify the following post-condition: I will ensure upon completion that the value of i will be one greater than its previous value.
class MyType
{
void MyAlgorithm (int i)
ensures i == old(i) + 1;
{
// ...
}
}In the previous code listing we use the Spec# keyword ensures to define the post-condition. We also make use of the special function old to acquire the original value of ipassed to the algorithm. We can use the Spec# throws keyword to specify the type of exception to throw upon failure to satisfy a post-condition.
class MyType
{
void MyAlgorithm (int i)
throws MyCustomException ensures i == old(i) + 1;
{
// ...
}
}To conclude our exploration of the Spec# language we will look at how one specifies type invariants. A type invariant is a property that must hold throughout the lifetime of an object, if the property fails to hold then the state of the object is deemed invalid. For example, specifying that the value of the m_count member within the List data structure should never be negative is a type invariant.
class List
{
// ...
int m_count;
invariant m_count >= 0;
{
// ...
}
}In the previous code listing we use the Spec# keyword invariant to specify a type invariant for the List data structure.We have only covered a small amount of what the Spec# language offers in this section.
In this section we will take a look at the code contracts library which will be shipped with .NET framework. The functionality that we will cover of the code contracts library are:
The associated tooling that ships with the code contracts library includes the ability to verify contracts at compile-time, as well as runtime checking. Further, the contracts specified can also be used to drive XML documentation.
Tooling to enable the generation of documentation from the code contracts specified is penned for a future release. All of the methods required can be found in the System.Diagnostics.Contracts namespace. You will need to reference the Microsoft.Contracts.dll found in the install directory of the code contracts preview from your project.
Before we look at some code we need to talk about a few property options that you can define. These properties can be defined by selecting the Code Contracts tab within the properties page of your C# project. We will look at two of the available properties in this tutorial. The first property, Runtime Checking allows us to enable the runtime checking of pre-conditions, post-conditions, and type invariants. The second property, Static Checking allows us to specify whether or not we want certain properties of our program to be checked at compile-time. For all the code listed in this section assume that we are using a debug build and that the following options are checked within the Code Contracts tab:
There are two tools that will be invoked now during a build of our code:
The two tools are not dependent on one another so depending on the options you define within your project properties then the correct tool(s) will be invoked during a build.
Just like in the Spec# section we will start by defining a non-null constraint, remember though that as we have static checking enabled we expect this precondition to be verified at compile-time.
using System.Diagnostics.Contracts;
namespace DotNetCodeContracts
{
class Program
{
static void Main()
{
MyAlgorithm(null);
}
static void MyAlgorithm(string word)
{
Contract.Requires(word != null);
}
}
}In the previous code listing we use the static method CodeContract.Requires to specify our pre-condition. If you build the code listing you will see that a warning is flagged with the textual description "requires is false".For our second example we will define a pre-condition that will not be flagged by the ccchecker tool, rather we will rely on the runtime verification code produced by ccrewrite.
using System.Diagnostics.Contracts;
namespace DotNetCodeContracts
{
class Program
{
static void Main()
{
MyAlgorithm(11);
}
static void MyAlgorithm(int i)
{
Contract.Requires(i > 0 && i < 10,
"i must be greater than 0 and less than 10");
}
}
}If you build the previous code listing then you will notice that the ccchecker tool does not complain about the pre-condition of MyAlgorithm not being satisfied. However, if you run the code an unhandled exception window will be presented alerting us that the pre-condition was not satisfied.
Post-conditions using the co de contracts library are simple to define. Moreover, the library provides a host of methods which allow for easy access to certain properties of an algorithm. The following code listing demonstrates the specification of a post-condition with the aid of some special methods exposed by the code contracts library.
using System.Diagnostics.Contracts;
namespace DotNetCodeContracts
{
class Program
{
static void Main()
{
MyAlgorithm(1);
}
static int MyAlgorithm(int i)
{
Contract.Requires(i > 10);
Contract.Ensures(Contract.Result<int>() ==
Contract.OldValue(i) + 1);
return i;
}
}
}In the previous code listing we make use of two special methods exposed by the co de contracts library: T Contract.Result<T>() and T Contract.OldValue<T>(T value). The first method allows us to reference the actual return value of the method, the second allows us to get the pre-state value of i. If you build the previous code listing you will get another “ensures unproven” message flagged as we have not proven sufficiently that the post-condition will be satisfied. Further, if you decide to disregard the warning message and run the program then you will be greeted with an unhandled exception window reaffirming that the post-condition has not been satisfied. The fix? Well, for this simple case all we need to do is exactly what we said we would do in the post-condition, we simply increment i by one.
using System.Diagnostics.Contracts;
namespace DotNetCodeContracts
{
class Program
{
static void Main()
{
MyAlgorithm(1);
}
static int MyAlgorithm(int i)
{
Contract.Requires(i > 10);
Contract.Ensures(Contract.Result<int>() ==
Contract.OldValue(i) + 1);
i++;
return i;
}
}
}For brevity this will conclude our look at the post-conditions within the code contracts library. However, the reader should be informed that we have only scratched the surface with respect to post-conditions in the code contracts library. More information on post-conditions can be attained via the manual that ships with the code contracts preview download.
Type invariants are easy to specify using the code contracts framework. It’s simply a matter of creating an appropriate method which will be automatically called to verify the invariant. In order to qualify, the method must:
ContractInvariantMethod attribute.The type invariant is checked upon all method exits and is assumed to hold upon on all method entries, this includes constructors.
using System.Diagnostics.Contracts;
namespace DotNetCodeContracts
{
class Program
{
static void Main()
{
List list = new List();
list.InvalidateState();
}
}
public class List
{
private int m_count;
[ContractInvariantMethod]
internal void ObjectInvariant()
{
Contract.Invariant(m_count >= 0);
}
public void InvalidateState()
{
m_count--;
}
}
}}In the previous code listing a type invariant is specified to ensure that the value of the member m count never has a negative value. If at any stage the type invariant fails to hold then an unhandled exception window is presented. All the type invariants you specify must be contained within the method decorated with the ContractInvariantMethod attribute.
In this section we will take a look at the ccrewrite tool. The tool itself is invoked when you specify that you want to perform runtime checks to verify pre-conditions, post-conditions, and type invariants. The ccrewrite tool injects pre- and post-conditions into the correct place as well as injecting other boilerplate code. To clarify this let us consider the following method:
static int MyAlgorithm(int i)
{
Contract.Requires(i > 10);
Contract.Ensures(Contract.Result<int>() ==
Contract.OldValue(i) + 1);
return i;
}After ccrewrite has been invoked the previous method looks like the following:
private static int MyAlgorithm(int i)
{
int Contract.Old() = i;
__RewriterMethods.RewriterRequires(i > 10, "i > 10");
int CS$1$0000 = i;
int Contract.Result<int>() = CS$1$0000;
__RewriterMethods.RewriterEnsures(Contract.Result<int>()
== (Contract.Old() + 1),
"...");
return Contract.Result<int>();
}Some things to note:
Contract.Old() is assigned the value of i immediately upon method entry;i, the method returns this value by calling T Contract.Result<T>(); andccrewrite has injected an internal class _RewriterMethods into the binary which comprises of five static methods: RewriterAssert(bool condition, string message), RewriterAssume(bool condition, string message), RewriterEnsures(bool condition, string message), RewriterInvariant(bool condition, string message), and RewriterRequires(bool condition, string message).Also it is worth noting that wherever you place your pre- and post-conditions in your method, ccrewrite will ensure these conditions are injected at the appropriate places, e.g. pre-conditions will be injected just after method entry (only preceded by other ccrewrite boilerplate code), and post-conditions will be injected just before method exit.I strongly advise that you become familiar with the code that ccrewrite injects into your binary. If you use code contracts liberally you will notice that ccrewrite injects an awful lot of code to help verify your contracts.
The Microsoft VC++ compilers allow you to specify pre- and post-conditions via the use of source annotations. As you might have guessed the VC++ source annotations are more low-level than those offered in the .NET code contracts library, this is to be expected as the needs of C++ programmers differ greatly from those of their C# counterparts. Source annotations are incredibly powerful and well worth using. However, before you can use source annotations in your C++ code you must:
CodeAnalysis\SourceAnnotations.h header file;vc attributes namespace into scope; and/analyze compiler switch which can be done via the Code Analysis tab of the project pages or via the command line to cl.exe.The steps are slightly different when using source annotations in C code.
Specifying a pre-condition using source annotations is straightforward, they take the form [Pre(Annotation Property)].
#include <iostream>
#include <string>
#include <codeanalysis sourceannotations.h>
using namespace vc_attributes;
// pointer must not be NULL
void MyAlgorithm([Pre(Null=No)] std::string* pWord)
{
// do something to the string...
}
int main()
{
std::string* pWord = 0;
MyAlgorithm(pWord);
return 0;
}In the previous code listing we apply a pre-condition to the pWord argument stating that the pointer must not be NULL. If you build the program you will see that a warning is flagged with the textual description "Warning C6387: 'argument 1' might be '0': this does not adhere to the specification for the function 'MyAlgorithm' "
A post-condition specified with the use of source annotations can be used to specify properties to assist the programmer calling the algorithm in question, e.g. we might specify that the programmer must always check the return value of the algorithm, or we might want to tell the programmer that the return value should not be checked against a particular value.
#include <iostream>
#include <string>
#include <codeanalysis sourceannotations.h>
using namespace vc_attributes;
[returnvalue:Post(MustCheck=Yes)]
int MyAlgorithm(int n)
{
// compute something for n...
return n;
}
int main()
{
MyAlgorithm(12);
return 0;
}In the previous code listing a warning will be flagged with the textual description “Warning C6031: Return value ignored: ’MyAlgorithm’ ” The following example specifies that the caller must check the value returned by MyAlgorithm, but not check it against the value 0.
#include <iostream>
#include <string>
#include <codeanalysis sourceannotations.h>
using namespace vc_attributes;
[returnvalue:Post(MustCheck=Yes)]
[returnvalue:InvalidCheck(Value=0)]
int MyAlgorithm(int n)
{
// compute something for n...
return n;
}
int main()
{
if (MyAlgorithm(12) == 0)
{
// ...
}
return 0;
}If you build the previous code listing you will notice that we no longer get a a warning about not checking the return value of MyAlgorithm. Instead, we get warned that we are checking the return value of the algorithm against a value which the algorithm designer has defined as being invalid, the following warning is raised "Return value for a call to 'MyAlgorithm' should not be checked against '0'.
This tutorial has shown you the benefits of using contracts within your code whether it be C# or C++. We started off by looking at Spec#, then proceeded to explore the new code contracts library shipping in .NET, and finally concluded with a brief look at the VC++ source annotations.
Code contracts allow you to be more explicit about algorithm behavior, and catch potential bugs early on. Use them whenever and wherever possible.