Summary: An introduction to the non-null types feature
Nearby: SpecSharpIntroduction, HomePage

Non-null types

Whether a pointer may be null or is definitely not null is a very common specification. To make it easy to specify that pointers are non-null, Spec# provides non-null types. For any reference type T, the type T! denotes a reference to a T that is definitely non-null. Such non-null types can be used wherever types occur with a few exceptions.

The type checker ensures that when a context expects a non-null value, the program actually supplies one. For example, when passing a possibly null value as the argument to a method whose parameter has a non-null type, the checker will complain.

C# Version

The following C# program causes a ""NullPointerException"" at run time. The null dereference error is not detected by the C# compiler.

		 class [MyLibrary]
		 {
		    public static void Clear(int[] xs)
		    {
		       for (int i = 0; i < xs.Length; i++)   // NullPointerException!
		       {
		          xs[i] = 0;
		       }
		    }
		 }
		 class [ClientCode]
		 {
		    static void Main()
		    {
		       int[] xs = null;
		       [MyLibrary.Clear(xs);]
		    }
		 }
	

Spec# Version

If you feed the same program to the Spec# compiler, it will detect the possible null dereferences.

		 class [MyLibrary]
		 {
		    public static void Clear(int[] xs)
		    {
		       for (int i = 0; i < xs.Length; i++)   // Warning: Possible null dereference
		       {
		          xs[i] = 0;   // Warning: Possible null dereference
		       }
		    }
		 }
		 class [ClientCode]
		 {
		    static void Main()
		    {
		       int[] xs = null;
		       [MyLibrary.Clear(xs);]
		    }
		 }
	

If you decide that it's the caller's responsibility to make sure the argument is not null, Spec# allows you to record this decision concisely using an exclamation point. Spec# will also enforce the decision at call sites.

		 class [MyLibrary]
		 {
		    public static void Clear(int[]! xs) 
		    {
		       for (int i = 0; i < xs.Length; i++)   // OK
		       {
		          xs[i] = 0;   // OK
		       }
		    }
		 }
		 class [ClientCode]
		 {
		    static void Main()
		    {
		       int[] xs = null;
		       [MyLibrary.Clear(xs);]   // Error: null is not a valid argument
		    }
		 }
	

If you prefer to keep your source code C#-compatible, you can enclose the exclamation mark in special brackets (""/^"" and ""^/""). The C# compiler interprets this as a comment and ignores it; the Spec# compiler ignores just the brackets themselves.

		 class [MyLibrary]
		 {
		    public static void Clear(int[]/*^!^*/ xs) 
		    {
		       for (int i = 0; i < xs.Length; i++)   // OK
		       {
		          xs[i] = 0;   // OK
		       }
		    }
		 }
		 class [ClientCode]
		 {
		    static void Main()
		    {
		       int[] xs = null;
		       [MyLibrary.Clear(xs);]   // Error: null is not a valid argument
		    }
		 }