Spec# 1.0.10718 for Microsoft Visual Studio 2005 Release Notes

Changes since last release

0. The new theorem prover Z3 is now part of the Spec# distribution! It is now the default theorem prover used by Boogie, so you no longer need to have Simplify installed. There is a command-line option to Boogie if you wish to continue using Simplify.
1. Non-null Element Arrays in Spec#
   0. It is now possible to specify a non-null element array. For example:
      

      string![] msgs = new string![200];
      

      Obviously after this statement, the array elements are null, even though the type appears to guarantee that they are non-null. Spec# prevents you from accessing elements of the array before it is fully initialized. That is done by calling a special library method:
      

      Microsoft.Contracts.NonNullType.AssertInitialized(args);
      

      This method inserts a run-time check that ensures every element of the array is non-null. If any of the elements are null, then an exception of type Microsoft.Contracts.NonNullType.NullException will be thrown. Calling this method is called commitment of the non-null element array. However, there is a subtle distinction between an array that is fully initialized and an array of which every element is non-null. Suppose we have objects that are not fully initialized and we use these objects in the initialization of the array elements. What is likely to happen is that after the commitment call, the array elements are still considered not fully initialized. In Spec#, such objects are called delayed objects. If you try to use a delayed object in a context that requires a non-delayed object, a warning will be generated. For example:

      class Foo {
        string! Name;
        void bar(Foo! [] foos) {
      System.Console.WriteLine(foos[0].Name); // to amplify this problem, we try to  
                                              // print foos[0].Name, which is still null
        }
        public Foo() {
      Foo! [] foos = new Foo[1];
      foos[0] = this;
      Microsoft.Contracts.NonNullType.AssertInitialized(foos);
      Bar(foos); // will have a warning
        }
      }
      

      Possible delayed objects include: self (this) in a constructor, other non-null element arrays that have not been committed, parameters that have an explicit attribute [Delayed], or any other objects that contain a reference to a delayed object.
   1. Compiler Generated Commit Calls In certain cases, non-null arrays are constructed without a new array operation. Most notably, we may have:

      string![] Arr = {“hello”};
      

      Or:

      void foo(params string! args[]) {
      }
      //...
      // at calling site
      foo(“hello”);
      

      For these cases, the Spec# compiler adds a commitment call for you.
   2. Generics If an array’s element type is a type parameter of a generic, the compiler needs to guarantee the correct use of such array when the type parameter is instantiated to a non-null type.

      T [] arr = new T [1];
      

      We require that , unless it is impossible for T to be instantiated to a non-null type (for example, there is a constraint that says T is a struct), the programmer must add a commitment call:

      Microsoft.Contracts.NonNullType.AssertInitialized(arr);
      

      We have overloaded AssertInitialized. NOTE: existing code may have to change.
   3. Possibly Null Type Parameter If you have existing code that does not expect T to be instantiated to a non-null type, the best bet is to change its type to possibly null by adding a question mark to T.

      T? [] arr = new T?[1]; // there is no need to have commitment call
      

      Note that possibly null type parameter is not nullable type, though they have the same syntax. Nullable types are not allowed as generic type parameters.
2. Lots of bug fixes and other features that will eventually be documented...