Spec# - Design by Contract

I have been reading about Design by Contract implemented in Eiffel, and after looking a bit around I came across Spec# this is an extension to C#. I especially like the Pre and Post conditions idea. At first it looked like you had to put these declarations with the object implementations, but after some testing and looking further I was pleased to see it is also possible to put these declarations at the interface level. Here is a simple example of a simple car object: Below is the interface ICar and as you can see there are some extra declarations that you would not have used before; requires and ensures. These are basically telling the user of the object that is based on the ICar interface that this object only accepts a certain input and guarantees a certain output.

Interface: ICar

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

using System; namespace CarFactory { public interface ICar { void Init(int wheels, string color) requires wheels == 3 || wheels == 4; requires color != ""; int Wheels { get; ensures result == 3 || result == 4; set; requires value == 3 || value == 4; } string Color { get; ensures result != ""; set; requires value != ""; } } }

Here is an implementation of the ICar interface in the form of an Audi object. Also in this object you see two new keyword; invariants and expose. The invariants define what a proper state of the object should be, and expose is to allow change of the object. While inside the expose block the object does not have to comply with the invariants but as soon as you are finished it should comply again.

Class: Audi

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35

using System; namespace CarFactory { public class Audi : ICar { private int _Wheels; private string _Color; public Audi() { _Wheels = 4; _Color = "Red"; } invariant _Wheels == 3 || _Wheels == 4; invariant _Color != ""; public void Init(int wheels, string color) { _Wheels = 4; _Color = "Red"; } public int Wheels { set { expose(this) { _Wheels = value; } } get { return (_Wheels); } } public string Color { set { expose(this) { _Color = value; } } get { return (_Color); } } } }

Using the object is like it was before:

Usage

1 2 3 4 5 6 7 8 9 10 11 12 13 14

using System; namespace CarFactory { public class Program { static void Main(string![]! args) { Console.WriteLine("Spec# create Audi!"); ICar audi = new Audi(); audi.Init(4, "Red"); Console.WriteLine("Spec# Audi has "+ audi.Wheels +" wheels and is "+ audi.Color +"!"); } } }

Now if you would violate the Design by Contract rules when accessing a property or method than you would get an exception at the rule defined in the interface. And if the object implementation violates the rules than you would also get the exception at the rule it break. Also read these following posts about Spec# by Matthew Podwysocki.