Spec# - Constraining the domain your c# program operates upon

I found this at Microsoft’s research downloads: Spec# is an extension to the c# programming language and brings multiple ways of adding explicit constraints to what is essentially the data your c# program works upon. One nice example from the overview[pdf] presented there:

class ArrayList {
  public virtual void Insert(intindex,object value)
    requires 0 <= index && index <= Count;
    requires !IsReadOnly &&!IsFixedSize;
    ensures Count == old(Count)+1;
  { /*...*/ }

Means that some preconditions are required: index is bigger than 0 and smaller than the current value of Count. Furthermore the fields IsReadonly and IsFixedSize should be false. The postcondition of the call is that the count field should have increased by 1.

This is just one of the features available. Those who like constraining their objects with pre- and post conditions (values and exceptions), more specific avoidance of null references and ways to state invariants should have fun with this (Does this include me? I s’ppose it depends on the project!)