Summary: Delayed types permit the Spec# Type System to reason about non-null typed fields during object initialization.
Nearby: NonNullIntroduction, SpecSharpIntroduction, HomePage

Fields of non-null type

When non-null types are used for fields, they act as object invariants. Reading such fields should always provide a non-null value and writing such fields can only be done with non-null values. In order to make such guarantees, the checker must ensure that all non-null declared fields of an object are initialized before any code could read them and observe the null value from the default initialization.
The compiler enforces the initialization of fields in one of two ways, depending on whether the constructor is delayed or non-delayed.

Delayed constructors

A delayed constructor treats this as a delayed reference, meaning that the constructor is only allowed to initialize the object pointed to by this, but does not actually read fields of the object. We call the this parameter of a delayed method a delayed reference. Delayed references can only be used to initialize fields of the delayed reference, or they can be stored into other objects that are themselves delayed. If a delayed reference needs to be passed to another method (as a explicit parameter or as this), then the method signature must guarantee that it treats the parameter as delayed by having the Microsoft.Contracts.Delayed attribute on the parameter (method for this). Thus, base constructors called from a delayed constructor must themselves be delayed.
By default, the compiler assumes constructors are delayed. To override this default, add the attribute Microsoft.Contracts.NotDelayed on the constructor. This is useful if the constructor does non-trivial computations using the fields of the object being initialized. Here’s an example of a delayed constructor.

		  class C {
		    string! name;
		    // A delayed constructor (default)
		    public C(string! n) {
		       this.name = n;
		    }
		  }
	

For delayed constructors, the compiler enforces that all non-null fields are initialized by the end of the constructor. This is sufficient, since the base constructor called (implicitly or explicitly) by a delayed constructor must also be delayed, thereby guaranteeing that fields will not be read (via virtual calls). Most constructors in programs are delayed. This property allows one to guarantee proper initialization of circular structures, meaning that all pointers on a cycle are actually non-null as in the next example:

		  class List {
		    Node! head;
		    public List() {
		      this.head = new Node(this);
		    }
		  }
		  class Node {
		    List! list;
		    Node! prev;
		    Node! next;
		    public Node([Delayed] List! list) {
		      this.list = list;
		      this.prev = this;
		      this.next = this;
		    }
	

}
The List constructor above initializes a field head to point to the initial sentinel of a doubly linked list. The List nodes themselves contain a pointer back to the list as well as prev and next pointers. As the example shows, we are able to declare all these fields with non-null types and the type checker guarantees that these fields are indeed initialized prior to reading them. Note that when the Node constructor is called with the List argument, the list itself is not properly initialized yet (the head field has yet to be assigned). But that is okay, since the Node constructor treats the List parameter as delayed (using the attribute Delayed), guaranteeing that it won’t yet observe any invariants about the list.

Non-delayed constructors

Some constructors do more than just initialize fields. They require calling other methods on the object being constructed that require reading of the fields. Such non-delayed constructors must be annotated with the attribute Microsoft.Contracts.NotDelayed. In non-delayed constructors, non-null declared fields must be initialized prior to the (implicit or explicit) base constructor call. The base constructor call demarcates the end of non-null declared field initialization. After that call, all non-null declared fields are properly initialized.
In C#, the base constructor call appears always at the beginning of the constructor (often implicitly). This makes it difficult to initialize fields that depend on constructor arguments. In Spec#, constructors can call the base constructor explicitly within the body of the method after initializing the non-null declared fields.

		  class C {
		     string! name;
	

		     public C(string! n) {
		       this.name = n;
		       base();  // explicit base call after the non-null field ‘name’ is initialized
		     }
		  }