Spec# 1.0.20411 for Microsoft Visual Studio 2005 Release Notes

Changes since last release

  1. Spec# now has support for ownership with generic classes, especially generic collections. The notation is very similar to element ownership for arrays. Fields whose range type is generic can have the [ElementsRep] and [ElementsPeer] attributes. For instance, one can declare a field [Rep][ElementsPeer] List<C> myList; With this declaration, the myList object is owned by “this”, whereas the elements in the list are peers of “this” (not peers of the list).

    In general, instances of generic classes are homogeneous w.r.t. the element owner. In other words, all objects stored in a generic list must have the same owner, even if no [ElementsRep] or [ElementsPeer] attribute is used. However, there is an important exception: If the type variable is instantiated with a type that is potentially immutable then the elements can have arbitrary owners. This is the case for immutable types, interfaces, and in particular class object. So a list of type List<object> is heterogeneous w.r.t. the class of the elements and the owner of the elements.

    Methods of generic classes have extra pre- and postconditions that ensure that the element owners are used properly. For instance, the call myList.Add(x); requires x to be owned by the element owner for myList. Analogously, x = myList[0]; guarantees that x is owned by that element owner. This is particularly useful to ensure that x is peer-consistent. Because we know from the declaration of myList that x is a peer of “this”, we can derive from the peer-consistency of “this” that x is peer-consistent and, thus, call methods on it. These pre- and postconditions have to be proven when the generic class is verified. So they make it easier to use generic classes, but harder to verify the implementation of generic classes.

    The element owner can be manipulated using methods of class Owner. This is done by obtaining an element proxy, which is a representative for all the objects that are stored in a generic collection. In other words, the element proxy is a peer of all other elements, which allows the other methods of class Owner to be applied to element owners. For instance, one can set the element owner of a collection by assigning an owner to the element proxy: Owner.Assign( Owner.ElementProxy(myList), o, T); This call will transfer the proxy of myList and all its peers (that is, elements stored in myList) to the owner [o,T]. Such a transfer happens automatically when a generic instance is assigned to a fields with an no [ElementsRep] or [ElementsPeer] attribute, like for ordinary ownership.

    Since classes can have several generic type arguments, [ElementsRep], [ElementsPeer], and Owner.ElementProxy also exist in overloaded versions that take an integer parameter indicating to which type argument the attribute or method applies. For instance, the declaration of myList can also be written as: [Rep][ElementsPeer(0)] List<T> myList; because ElementPeer applies to the type argument at position 0. A dictionary could for instance map strings to rep objects of class C: [Rep][ElementsRep(1)] Dictionary<string, C> myMap; Note that the first type argument here is immutable and, thus, does not need a specification of the corresponding element owner.

    The current implementation still has limitations. The two most important are:
    1. The admissibility checker for invariants does not recognize [ElementsRep] and [ElementsPeer]. For instance, the invariant myMap[”key”].someBooleanField is an ownership-based invariant because myMap and myMap[”key”] are owned by “this”. However, the admissibility checker rejects this invariant.
    2. Verifying the implementation of a generic class typically requires invariants about the element owners. Currently, these invariants are not generated automatically (unlike the pre- and postconditions for methods of generic classes); one has to use the methods of class Owner to specify them explicitly.
  2. Quantifications over arrays can now be written as Q{int x in A; P(x)} where Q is any of the quantifiers, e.g., forall or exists. This is in addition to the existing notation: Q{int i in (0:A.Length); P(A[i])}.
  3. The attributes [Confined] and [StateIndpendent] have been made obsolete. Now all pure methods are annotated with [Pure]. In addition, you may want/need to restrict what the pure method is allowed to read in the heap. For this, a new attribute [Reads] has been introduced: [Reads(ReadsAttribute.Reads.Owned)] indicates that the method reads values from the heap only from objects that it owns. [Reads(ReadsAttribute.Reads.Nothing)] indicates that the method does not read anything at all out of the heap (or at least, not any mutable state in the heap). There is also [Reads(ReadsAttribute.Reads.Everything)] that allows the pure method to read anything from the heap. When a method is marked just with [Pure] and not Reads attribute, then the defaults are:
    instance method in a class [Pure][Reads(ReadsAttribute.Reads.Owned)]
    instance method in a struct [Pure][Reads(ReadsAttribute.Reads.Nothing)]
    static method [Pure][Reads(ReadsAttribute.Reads.Nothing)]

    Property getters are assumed to be pure unless otherwise indicated.
  4. Many other improvements that are sure to be documented any day now...