One of the key characteristics that makes a professional-quality application is defensive coding. While necessary, this can hide the meaningful portions of logic. It can also lead to many tests that are more related to the chosen implementation than the business rules. Take this simple piece of code to add a word to a sentence.
public void AddWord(string word)
{
if (word == null) throw new ArgumentNullException("word");
if (word.Length == 0) throw new ArgumentException("word");
words.Add(word);
}
The validation code dominates this simple function. Additionally it does not provide the consumer of the method with any hints to the parameters constraints. Sure, xml docs can provide some documentation, but that still does not help at design time. A set of tests that check the expected exception would also be common for this block of code. There is plenty to debate about the non-functional tests, but it is safe to assume that this kind of testing is common.
The Spec# team is doing some incredible work to make constraints like this either enforced by the language or more visible by placing them within the method signature.
The first parameter check relates to nullness. Spec# provides an operator for forcing non-null. The signature of AddWord would now look like:
public void AddWord(string! word)
This tells the compiler and Visual Studio that this parameter cannot be null. If you even try to pass a string that can be null to this method, a warning will appear at design time. A compiler error will also result. This really cranks up the visibility of the constraint. The user of this method can also see the constraint right in the signature.
The second parameter check relates to some data constraint on the string. In this case, it is required to be a non-empty string. What is really going on here is that this method has a pre-condition relating to the data it is going to work with. Preconditions in Spec# are specified with the requires keyword. So our method now looks like:
public void AddWord(string! word)
requires word.Length > 0;
{
words.Add(word);
}
Now the requirements are part of the method signature that show up in intellisense. This alone is a big help to the development process. The precondition is validated at runtime kicking out an exception if the condition is not met. It is worth noting that you can map the stock RequiresException back to an argument exception via the otherwise keyword.
requires word.Length > 0 otherwise ArgumentException;
It is pretty evident to see the big gain here in the signature of the method containing all of the relevant constraints. Even more assistance can be provided at design and compile time when these constraints are provided in the signature. Even better than all of this is that the body of the method is left with only the required logic the method is responsible for.
There is plenty more to cover with the direction spec# is taking. Next up, validating the internal state of an object as part of the class definition.