See Installing Simplify.
Our changes do not have much impact on run-time checking, except that we've improved the conditions we check as default preconditions (you may say the previous checks were somewhat buggy). The changes do affect static verification with Boogie, as we describe next.
Our new form of the expose statement, which we call
local expose or non-additive expose, has the syntax:
expose(o at T){...}
where T is a (not necessarily proper) superclass of the static type
of o. We refer to the previously supported expose(o){...}
block as an additive expose.
Remember that the Boogie methodology divides the state of an object into class frames, according to the class that declares each field. Each class frame is exposed or not. With additive expose, an object must be exposed one class frame at the time, beginning from the dynamic type of the object and going toward superclasses. With local expose, you are allowed to "locally" expose any class frame that isn't already exposed. This means you won't see that pesky "Object might not be exposable" error message nearly as often.
A local expose can thus be started more often than the additive expose, but it isn't as powerful. In particular, inside a local expose at a class T, you can update only the non-additive fields of T. A field is non-additive if it is private or if it is declared with the attribute [Additive(false)].
There are also other restrictions. We only allow each object to have one local expose in progress at any time. Also, while you can invoke methods on rep objects inside a local expose (that is, on objects owned by the object that is locally exposed), you cannot generally invoke methods on this (including base calls) or on peer objects. To make such calls, first end the local-expose block.
The implementation in a class T of a virtual method (declared in T or a supertype) gets a default precondition that says the receiver is exposed for all class frames that are proper subclasses of T. This is exactly the precondition you need in order to do an additive expose on this inside the implementation. But, as alluded to above, this means you can't call other methods on this or its peers. If you do want to make such calls, or if you want to use a non-additive expose inside your method implementation so that you can modify non-additive fields, then you would prefer the virtual method to have the precondition that this is peer consistent. You can achieve that simply by marking your virtual method with [Additive(false)], which changes the default precondition for the virtual method (including all of its implementations) to this.IsPeerConsistent.
The name additive comes from the fact that it allows subclasses to reuse the
fields in superclasses, adding invariants about those fields, and overriding methods
as appropriate to make sure the fields satisfies their added invariants. While this
extensibility is in the spirit of object-oriented programming, it seems that most
programs don't make use of this flexibility (possibly in part because planning for
extensibility, especially without good tool support, is difficult). To make
Spec# easier to use for the more common cases, it seems it would be nicer to have
non-additive be the default (for fields, expose statements, and virtual methods).
In the Spec# release after this one, we hope to switch this default. Our
plan is to change the syntax of local expose to just
expose(o){...}
and to make the syntax for an additive expose be
additive expose(o){...}
In addition, fields and virtual methods would be non-additive by default, so you would
have to mark them as [Additive] if that's what you want. We perceive that
changing the default in this way will improve usability, but it means you'll have to
be explicit about when you are planning for subclass extensibility (which, one can
argue, is what C# settled for anyway by making methods non-virtual by default).
But you'll need to wait for the next release to see this change of defaults.
Until then, you're welcome to provide us with feedback on additive versus non-additive.
The word Immutable suggests that the fields of an Immutable object cannot change after the constructor has run. This is almost true, except that we do allow updates to fields that are not mentioned in invariants (something we probably will change before the next release). What we mean by Immutable is that, after construction, the object remains consistent forever (that is, the object's invariants always hold). Furthermore, we enforce that Immutable objects have no peers, which means that Immutable objects are always peer consistent. This means you can invoke methods on them without having to keep track of peer consistency some other way. (In contrast, for mutable objects, you typically mark some fields as rep (with [Owned]) or peer (with [Owned("peer")]) to keep track of peer consistency.)
We still don't have direct support for fields that are assigned only once when that one time happens after the constructor has finished.