Summary: This topic introduces assertions, the most basic type of specification in Spec#.

Assertions are checks placed in code regarding the expected dynamic (i.e. run-time) state at a particular execution point. They have been a part of C# via the System.Diagnostics.Debug namespace, which allowed for coding of boolean expressions that could be checked at run-time. If evaluation of the boolean expression yielded a false result, then a run-time exception was raised.

In Spec#, an explicit language construct has been added via the AssertStatement. This statement begins with the keyword assert followed by a boolean expression. If the boolean expression evaluates to false, an exception is raised.

As an example, the language evolution of checking that a reference is not null can be used:

C#

		 public void DoSomething(Node node)
		 {
		 	if ( node == null )
		 	{
		 		throw ApplicationException(...);
		 	} else {
		 		// normal processing continues
		 	}
		 }
	

System.Diagnostics.Debug.Assert

		 public void DoSomething(Node node)
		 {
		 	System.Diagnostics.Debug.Assert(node != null);
		 	// normal processing continues
		 }
	

Spec# assert

		 public void DoSomething(Node node)
		 {
		 	assert node != null;
		 	// normal processing continues
		 }
	

One of the benefits of elevating assertions to a language construct is that this approach allows for stricter semantics than System.Diagnostics, and aids static checking for program correctness.

For an even better way to specify that a reference must not be null, see NonNullIntroduction.