Spec# 1.0.5626 for Microsoft Visual Studio 2005 Release Notes

Installing Simplify

See Installing Simplify.

Changes since last release

  1. Attributes introduced by this version:
  2. A new compiler option, /checkcontracts (/cc for short) has been added. The default is for it to be on; turn it off by specifying /checkcontracts- on the command line. In the Spec# project properties, it is listed under the Configuration Properties as CheckContractAdmissibility. In the C# project Contracts pane in the project properties, it is listed in the "Compile time checks" section as "Check contract admissibility".
    When on, the compiler performs a static check to make sure that all members referenced in contracts are allowed to be mentioned. (Some accessibility checks had already been implemented making sure that members are as visible as the methods to which the contracts are attached and that methods were annotated as pure.) For instance, only owned fields may be mentioned in an object invariant. Also, if methods are used in a contract, they must not induce a circularity. Find below a detailed description of the admissibility rules. 
    Invariant admissibility
=======================

An invariant declaration in class C is admissible if every field
access, array access, method call and quantification is admissible.
For simplicity, gi and f may refer both to field accesses and method calls.

1. Field access and method call admissibility

Expressions in invariants can contain Confined and StateIndependent
method calls. Ownership information for these methods is derived from
the explicit rep and peer annotations as well as from the Element and
ElementCollection attributes together with the ElemensRep and
ElementsPeer attributes on the receiver object.
Parameters of method calls must be admissible.

Access chains of the following forms are admissible.

  (1) this.g1.g2...gn.f, where 
        either 
          n=0, 
        or 
          g1 is marked rep and each of g2,...,gn is either marked rep
          or a peer.

  (2) this.g1...gn.f, where n>=1, and 
          f is a field that mentions C in its Dependent attribute
          (visibility-based access),
        or
          f is a readonly field,
        or
          f is a field declared in an immutable type,
        or 
          f is a StateIndependent method.
      Furthermore, this.g1...gn is admissible.

  Additionally: 
    - In both cases, if g1 is a field access then it must be declared in class
      C or a supertype of C. In the latter case the field must be marked
      Additive.

    - Confined static methods are not admissible. As a consequence,
      methods Owner.Is, Owner.Same, Owner.None cannot be used in
      invariants.

    - There is no admissibility requirement on targets and parameters of
      static and StateIndependent methods.


2. Array access admissibility

The admissibility rules for accesses that contain array accesses are as
follows:

  (1) this.g1.g2...gn.arr[i], where 
        either 
          n=0 and arr is a rep field,
        or
          g1 is a rep field and each of the fields g2,...,gn,arr is
          either a rep or a peer field.

  (2) this.g1.g2...gj.arr[i].gj+1...gn, where n>=1 and one of the
      following applies:
          j=0 and arr is a rep and ElementsRep field and gj+1,...,gn
          is admissible,
        or
          g1 is a rep field and each of the fields g2,...,gj,arr is
          either a rep or a peer field and arr is an ElementsRep field
          and gj+1,...,gn is admissible. Field arr may be ElementsPeer
          too provided the ownership-depth of the array object
          is greater than one.
        or
          C is mentioned in the dependent-clause of gn.


3. Quantification admissibility

  (1) forall{int i in (E1:E2); P(i)}, where E1, E2 and P(i) are admissible.

  (2) forall{T t in this.g1...gn.f; P(t)}, where the type of f is
        array-type or IEnumerable-like type, 
      and
        either n=0 and f is a rep field or g1 is a rep field and each
        of the fields g2,...,gn,f is either a rep or a peer field. 
      and 
        f is an ElementsRep field or an ElementsPeer field provided
        that the ownership-depth of the object refered to by f is
        greater than one.
      and
        P(t) is admissible, where t is considered to be rep.

Admissibility of target objects
-------------------------------

Target-objects of field and array accesses, and method calls must be
the implicit or explicit this-object or a member binding. Expressions
other than type-casts and nonnull-casts are not admissibile.
   

Specification admissibility of pure methods
===========================================

1. Since axioms are generated from the specification of pure methods,
   the specifications are only admissible if they are well-founded.

   To ensure the well-foundedness of method specifications, for each
   method call occuring in the specification there has to be a measure
   that decreases relative to the method being specified.

   The following measures are considered:

   (1) purity level: a method call with a purity level lower than the
       purity level of the method being specified is considered
       well-founded.
       The levels in decreasing order are: Pure, Confined,
       StateIndependent.

   (2) ownership of receiver of the method call: if the receiver of
       the method call that occurs in the specification is owned by
       the this-object then the call is considered well-founded.

   (3) the value of RecursionTermination attribute: if the
       RecursionTermination value of a method call is less than the
       RecurstionTermination value of the method being specified, then
       the call is considered well-founded.

   In case there is no decreasing measure found, there is a warning 
   issued, furthermore, the specification is not used for axiom
   generation.  

2. Besides well-foundedness, the following requirements apply.

   The specification of Confined methods must be Confined: the
   admissiblity rules are similar as for invariants, except that
   visibility-based accesses are not admissible. Only Confined and
   StateIndependent method calls may occur in the specification.

   The specification of StateIndependent methods must be
   StateIndependent: only readonly field accesses and field accesses
   on fields declared in immutable types are allowed. Only
   StateIndependent method calls may occur in the specification.

3. The following methods may not occur in the specification of
   Confined and StateIndependent methods: IsExposable, IsExposed,
   IsConsistent, IsPeerConsistent, IsValid, IsPrevalid.
  3. A new compiler option, /checkpurity  (/cp for short) has been added. The default is for it to be off; turn it on by specifying /checkpurity+ on the command line. In the Spec# project properties, it is listed under the Configuration Properties as CheckPurity. In the C# project Contracts pane in the project properties, it is listed in the "Compile time checks" section as "Check method purity".
    When on, the compiler does a static data-flow analysis to check that methods annotated as pure are indeed pure.
  4. Fixed a precondition on System.Array.Clear that was reported by Benjamin Lutz (thanks!). The correct precondition is now:
             requires array.Length - (index + array.GetLowerBound(0)) >= length otherwise ArgumentException;  
  5. As mentioned in the release notes of our previous release, fields and methods and expose blocks are now non-additive by default.  To use a field in the invariant of a subclass, declared the field with [Additive].  To expose an object so that you can modify an additive field, use additive expose (o) { ...}.  To get the right method precondition that allows you to do such an additive expose, use a virtual method and mark it with [Additive].
  6. Increased support for complete case information for subtypes:  Consider the following example:
        ... class LispNode { ... }
        ... class Atom : LispNode { ... }
        ... class Composite : LispNode { ... }
    The following program pattern is common:
        void M(LispNode! n) {
            if (n is Atom) { ... }
            else if (n is Composite) { ... }
            else { assert false; }
        }
    The correctness of this code relies on that every LispNode is either an Atom or a Composite.  This is known to be so if:
    7. Boogie now understands these things.
  7. The BoogiePL language now supports indexed type families, which in a type-safe way reduces the number of explicit cast expressions needed in BoogiePL programs.  Previously, you might (as Boogie's translation of MSIL into BoogiePL does) have encoded the heap as:
        var Heap: [ref,name]any;
    that is, as a map from object identities and field names to the values of these fields.  Field names are then declared as constants:
        const f: name;
    and reading and updating a field may look as follows, if f is an integer field:
        x := cast(Heap[this, f], int);
        Heap[this, f] := x;
    Note the awkward (and not type-safe) cast, and note that mistakes of assigning non-integers to Heap[this, f] are not caught.  With the new BoogiePL, you can declare these things as follows:
        var Heap: [ref, <t>name]t;
        const f: <int>name;
        x := Heap[this, f];
        Heap[this, f] := x;
    The type of Heap is in more standard type notation written as:  (forall t :: [ref, <t>name]t).
  8. Boogie's output now also says how many verifications succeeds and, if any, how many were inconclusive or ran out of time
  9. Increased support for verifying implementations of pure methods, with respect to whether or not objects are Committed.
  10. Quantifiers in BoogiePL can now be decorated with key-value pairs.  Currently, only the nopats key is interpreted (previously, it had a different syntax).  The idea is that these key-value pairs can be used by various theorem provers in theorem-prover specific ways.  A value in a key-value pair is either a BoogiePL expression or a string.  Here are two examples:
        (forall r: ref ::  { fnur: F(r,3) }  ... }
        (forall x: int, y: int, z: int, n: int ::  { qname: "Fermat's Theorem" }  ... }
  11. For every pure method M there is a corresponding #M function declared and axiomatized. The axiom provides information on the return value in case the precondition of the method is satisfied. In particular, the axiom lets one derive that the result is allocated, is of the appropriate type, and is peer consistent. Furthermore, one can derive the user supplied postcondition in case it is sound to axiomatize the postcondition.
    It is considered to axiomatize the postcondition in a sound way if the postcondition is satisfiable. That is, there is a witness which satisfies the postcondition. Unfortunately Simplify does not work well for proving the existence of such witnesses, thus there is a heuristic implemented that decides whether a witness surely exists, in which case the postcondition is axiomatized. The heuristics consider a postcondition safe to axiomatize if and only if one of the two cases apply:
  12. To enhance the reasoning capabilities about Confined methods, a new field, "exposeVersion", has been introduced. The declaration type of the field is System.Object and it is used to keep track of state changes of objects and their ownership cones.
    The value of the field is havoced at every unpack statement, that is, at the beginning of every expose block. Furthemore, the field is havoced at every field update, o.f = E, where it is statically known that f does not occur in any invariants, in which case the compiler does not require the update to occur inside an expose block.
    A method call havocs the exposeVersion of the receiver. Furthermore, if the method has a location of the form this.f1.f2...fn in its modifies-clause then the exposeVersions of objects this.f1, this.f1.f2, ... , this.f1.f2...fn-1 also gets havoced.
    If the exposeVersion of an object o is the same between two program points P1 and P2 then the state of the object and its ownership cone has not changed between P1 and P2. This property is exploited for Confined methods which yield the same return value in P1 and P2 since such methods may only depend on the state of the receiver and its ownership cone.
  13. By default pure methods may return newly allocated objects (MRNAO) and may perform reference comparison.
    In order to prevent the discrepancy between runtime assertion checking and static verification for assertions like "M() == M()" where M might return a newly created object, we enforce the following rules. To enforce the above rules, every expression needs to be classified to be MRNAO or not. This is done the following way:
  14. The syntax "o.**" can be used in a modifies clause. It means that all fields of all peers may be modified by the method.  (The Boogie support for .** came a few hours too late to make it into this release.) 
  15. Having a postcondition that can be statically determined to always fail (such as "ensures false") now gets correctly handled and (obviously) fails verification.
  16. Various bug fixes