Spec# 1.0.5818 for Microsoft Visual Studio .NET 2005 (RTM) Release Notes
Installing Simplify
See Installing Simplify.
Changes since last release
-
The default for whether reference types are non-null or not can be set as a
compiler option. (In the future we will probably make non-null the default, but
for now "possibly null" is the default.) When reference types are non-null by
default, then "T?" designates the type of a value that is either of type T or
null. The compiler option is "/nn"; there is also a check box in the project
properties (either in Spec# project files or in the Contracts pane of C# project
files).
-
In order to avoid putting explicit base constructor calls in constructors of
classes that contain non-null fields, we now assume that all constructors are
Delayed constructors. A delayed constructor stores values into fields of
"this", but does not read them. A delayed constructor is allowed to call its
base constructor before initializing non-null fields because it is "well
behaved". To mark a constructor as not delayed, use the attribute
Microsoft.Contracts.NotDelayed.
-
The non-null analysis has been strengthened quite a bit.
-
"Peer" support has been added. A peer is a non-owned object that an object has a
reference to. The field that holds the reference is called a "peer field". Peer
fields are now the default. The default precondition for every method is that it
is "peer consistent". Peer consistency is that all objects which are peers are
equi-consistent. This means that if the method's precondition is met, then it
can turn around and call methods on objects "this" holds references to (that
also have the same precondition) as long as it is not within an expose block.
-
Many bug fixes...