Summary: Small example programs illustrating the non-null types feature

This page showcases Spec#'s non-null types feature.

C# Version

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

		 using System.Collections.Generic;
		 class [MyLibrary]
		 {
		    public static void Clear(int[] xs)
		    {
		       for (int i = 0; i < xs.Length; i++)   // NullReferenceException!
		       {
		          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.

		 using System.Collections.Generic;
		 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.

		 using System.Collections.Generic;
		 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
		    }
		 }