Code Contracts

by Stefan 18. May 2010 14:29

Das .NET-Framework 4 enthaelt einen neuen Namespace: System.Diagnostics.Contracts

Die noetige Integration in Visual Studio muss aber erst heruntergeladen werden: http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

Nach der installation hat man in den Projekt-Eigenschaften eine neue Option, wo man Code Contracts aktivieren kann:

Zum herumspielen mit Code Contracts habe ich ein kleines Projekt gemacht. Die Idee: Auf einer 2D-Karte, die aus Pixeln besteht, laufen "Bugs" herum. Dabei kann jeder Pixel nur ein einziges mal besucht werden. Spannend wird es, wenn man verschiedene Bug-Implementierungen ausprobiert oder gegeneinander antreten laesst. Um dafuer zu sorgen, dass sich jeder Bug an die Spielregeln haelt, ist Code Contracts bestens geeignet.

Zunaechst aber erstmal ein paar einfache Beispiele, wie Code Contracts dabei hilft, die grundlegenden Rahmenbedingungen "abzusichern". Code Contracts funktioniert auf 2 Ebenen: Laufzeitpruefung und statische Pruefung. Bei der Laufzeitpruefung werden, wie der name schon sagt, die vorgegebenen Bedingungen zur Laufzeit geprueft. Interessanter ist jedoch die statische Analyse. Man braucht das Programm nicht einmal auszufuehren um moegliche Probleme zu erkennen. Ich haette nicht gedacht, wieviel ich bei der ersten Implementierung uebersehen hatte, bis mich Code Contracts darauf hinwies.

Fangen wir an mit Object Invariants. Dazu schreiben wir eine Methode, die mit dem [ContractInvariantMethod]-Attribut markiert wird und geben dann Bedingungen an, die immer gelten sollen. Diese werden am ende jeder Public Method getestet (es sei denn, der Aufruf kam aus der Klasse selbst):

    public class Map
    {
        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(Width > 0);
            Contract.Invariant(Height > 0);
            Contract.Invariant(_pixels != null);
        }

        private readonly Pixel[,] _pixels;

        public int Width { get; private set; }
        public int Height { get; private set; }

Wenn wir nun einen Konstruktor anlegen wuerden, ohne darin Width und Height zu setzen, wuerde Code Contracts bereits meckern. Deshalb schreiben wir den Konstruktor so:

        public Map(int width, int height)
        {
            Contract.Requires(width > 0);
            Contract.Requires(height > 0);
            
            _pixels = new Pixel[width,height];

            Width = width;
            Height = height;
        }

Wichtig ist hier die aufrufe an Contract.Requires(). Zur Laufzeit werden hier die Werte getestet. Findet Code Contracts bei der statischen Pruefung Code, bei den nicht sichergestellt ist, dass er gueltige Parameter uebergibt, so gibt es bereits da eine Warnung.

Vertraege funktionieren in beide Richtungen. Hier zum Beispiel verspricht der Aufruf, dass er nicht null zurueckgibt, dafuer verlangt auch er ordentliche Werte: 

        public Pixel this[int locationX, int locationY]
        {
            get
            {
                Contract.Requires(locationX >= 0);
                Contract.Requires(locationY >= 0);
                Contract.Requires(locationX < Width);
                Contract.Requires(locationY < Height);

                Contract.Ensures(Contract.Result<Pixel>() != null);

                return _pixels[locationX, locationY] ?? (_pixels[locationX, locationY] = new Pixel());
            }
        }
    }

So viel erstmal dazu. Demnachst gibt es noch mehr. Dann beschreibe ich wie man die Anforderung "Jedes Feld darf nur einmal besucht werden" umsetzt. Es ist erstaunlich wie weit da bereits die statische Pruefung einen Einblick in die Logik verschafft und Denkfehler aufzeigt, die einem sonst nicht aufgefallen waeren.

enjoyed the post?

Tags:

Add comment

  Country flag

biuquote
  • Comment
  • Preview
Loading

About Oliver

shades-of-orange.com code blog logo I build web applications using ASP.NET and have a passion for javascript. Enjoy MVC 4 and Orchard CMS, and I do TDD whenever I can. I like clean code. Love to spend time with my wife and our children. My profile on Stack Exchange, a network of free, community-driven Q&A sites

About Anton

shades-of-orange.com code blog logo I'm a software developer at teamaton. I code in C# and work with MVC, Orchard, SpecFlow, Coypu and NHibernate. I enjoy beach volleyball, board games and Coke.