Summary: A short explanation of how to program in Spec#: default preconditions, attributes needed for annotatons, and pure methods.

Common methods and constructors

By default, all in- and ref-parameters (or reference type) should be “peer consistent” on entry to methods, and all ref- and out-parameters and return values (of a reference type) should be “peer consistent” on exit from methods. An object is “consistent” when the constructor has finished running on the object, the object is not exposed, and the object either has no owner or the owner is exposed. A vital property of Spec# is that when an object is “consistent”, then its object invariant holds.

An object is “peer consistent” if it and all of its peers (that is, all other objects with the same owner) are consistent. (For the purposes of this paragraph and the previous, the receiver object of a constructor is not considered to be a parameter of the constructor.)

Some methods expect one of its parameters to already have been exposed by the caller. To specify this situation, mark the parameter with the @Inside@ attribute. To specify that the receiver parameter has already been exposed by the caller, place the @Inside@ attribute on the method itself.

If a field @f@ is mentioned in an invariant or is a @Rep@ field, then assignments to @f@ are allowed only when the target object is exposed. This means you must enclose the assignment within a Spec# expose statement. For example, @expose (this) { f = e; }@. The object invariant is checked at the end of expose block.

A field (of a reference type) can optionally be marked with the attribute @Rep@, saying that it points to a representation object, or @Peer@, saying that it points to a peer object (these attributes are declared in Microsoft.Contracts). If a field is not marked with either attribute, then the field itself does not say anything about whether or not the object it references is peer consistent, which means you’re likely to get a precondition violation “object is not peer consistent” if you try to invoke a method on the field. In such a situation, mark the field as @Rep@ if the field points to an object that is a private implementation detail of the enclosing class, or mark it as @Peer@ if clients of the enclosing class have any business knowing about the object.

When you assign an object, say @o@, to a rep or peer field of another object, say @t@ (that is, when you perform an assignment @t.f = o;@), then the owner of @o@ will be set to @t@ (if @f@ is a @Rep@ field) or to the owner of @t@ (if @f@ is a @Peer@ field). However, we currently only allow owners to change from None to a particular owner; that is, in assignments like these, we don’t allow @o@ to already have an owner that is different from the one that implicitly will be assigned as just described. In some cases, it may be necessary to assign owner manually, in which case you use the @Owner.Assign@ and @Owner.AssignSame@ methods (declared in Microsoft.Contracts).

By default, a method body is not allowed to change the owner of its parameters (or of any other previously existing object). To declare that a method may change the owner of a parameter, mark the parameter with the @Captured@ attribute. If it is the receiver object that is being captured (which sometimes happens, for example, if the constructed object is to become a peer of an object passed in as another parameter), then mark the method (or constructor) with @Captured@. Note that the @Captured@ attribute does not force the method to change any owner. If a method wants to advertise the new owner of a captured parameter, or indicate in which cases the parameter is not being captured after all, it can use the @Owner.Is@, @Owner.Same@, @Owner.None@, or @Owner.New@ methods in its postcondition.

When an object is peer consistent, so are all of its peers. Thus, if a method wants to invoke a method on one of its peer fields, it can just do so (without performing any expose operation). If the method wants to invoke a method on a rep field, then it must first do an expose operation. For example, if @f@ is a @Rep@ field, one might do: @expose (this) { f.M(); }@. When this expose statement changes @this@ from consistent to exposed (a state to which we sometimes also refer as “mutable”), the rep object becomes peer consistent, which is what’s needed to satisfy the precondition of the called method.

In some cases, a parameter is passed down to a method invoked on a rep object. For example:

		    public void M(C! c) { expose (this) { f.M(c); } }
	

where @f@ is a @Rep@ field. Here, the verifier will complain that @c@ might no longer peer consistent at the time @M@ is invoked; this complaint is warning about the situation when @c@ is a peer of @this@. To specify that @this@ and @c@ are not peers, use @Owner.Different@ in the precondition of @M@. (Note, use @Owner.Different(this, c)@, not the precondition @!Owner.Same(this, c)@. To the static verifier, these are equivalent, but since currently we don’t track ownership at run time, both Owner.Same and Owner.Different simply return true at run time. Hence, negating Owner.Same will always evaluate to false at run time, throwing a precondition-violation exception. We would like to implement a check in the compiler that makes sure that methods like these are used only in “positive” positions, but have not yet done so. Using these routines in positive positions goes well with the Spec# approach of being less strict in the checks performed dynamically than in checks performed by the static verifier.)

Pure methods

If you want to call a method in a specification, then the method called must be pure, which means it has no effect on the state of objects allocated at the time the method is called. To say that a method a pure, mark it with @Pure@, @Confined@, or @StateIndependent@. Each of these attributes says that the method is pure, and each also says something about what the method may read: a @Pure@ method may read anything, a @Confined@ method can only read the state of the receiver object and its (transitive) representation objects, and a @StateIndependent@ method does not read any mutable part of the heap. (From the fact that a method can be pure without being marked @Pure@, you can tell that we have some work to do in our naming of things. Indeed, we are planning on renaming all of these to @Pure@, and instead using a second attribute that says what the method may read. The default read permission will then be the one that corresponds to @Confined@ today. So, until we have implemented this name change, you probably want to mark most of your pure methods with @Confined@.)

Unless specified differently, every property getter is implicitly marked with @Confined@.

Pure methods don’t have the default “peer consistent” pre- and postconditions. Let’s say that an object is “fully valid” if it has been fully constructed and it is currently not exposed. That is, an object is “consistent” if it is “fully valid” and its owner is exposed. Stated yet another way, the difference between “consistent” and “fully valid” is that being “fully valid” does not say anything about the owner object. Analogous to “peer consistent”, we can now say that an object is “peer fully-valid” if it and all of its peers are fully valid. For a pure method, the default pre- and postconditions are that all parameters (on entry, for in- and ref-parameters, and on exit, for ref- and out-parameters) and return values are “peer fully-valid”, not “peer consistent” as for non-pure methods.

One consequence of this more liberal precondition on pure methods is that an owner does not need to be exposed when invoking a pure method on a rep object. For example, if @f@ is a @Rep@ field and @P@ is a pure method, then one can write:

		    public void M() { f.P(); }
	

Note that the return value of a pure method is (only) peer fully-valid. If the caller of a pure method P wants to invoke a regular method N on the returned object, as in:

		    o = t.P();  o.N();
	

then the static verifier will complain that the “peer consistent” precondition of the regular method @N@ is not satisfied. To specify that @P@’s callers are allowed to invoke @N@ on the returned object, you can explicitly add the postcondition @result.IsPeerConsistent@ to @P@. Alternatively, you can change @P@’s specification to say something about the owner of the returned value. For example, if @P@ has postcondition @Owner.Same(this, result)@ in the example above, then @o@ is peer consistent if @t@ is. Note that in the absence of any explicit postcondition of @P@, the call to @N@ is allowed if @N@ is also pure. This means, for example, that values returned from property getters (which, remember, are implicitly marked with @Confined@) can be used as arguments to pure methods, but nothing else; this gives a way to return an object that the caller, in effect, cannot modify.

Objects of some classes (like System.String) remain peer consistent forever, once their constructor has finished. If a type is marked with the attribute @Immutable@, then its objects are not allowed to be modified after construction. Consequently, just knowing the @Immutable@ type of an object is enough to know that the object is peer consistent. Class System.String is @Immutable@, so programs can always invoke methods on strings, because their “peer consistent” precondition will always hold. To enforce that immutable objects are “ever peer consistent”, the static verifier checks that no expose operation is applied to such an object. It also makes sure that immutable objects have no peers (because exposing such a peer would then violate the immutable object’s “ever peer consistent” characteristic). Consequently, a @Peer@ field is not allowed to hold an immutable object. (A problem we currently don’t have a good solution to is what happens when you want to have a @Peer@ field whose type is an interface type—for values of the interface type, it may not be known whether or not it is of an @Immutable@ type.) And, an immutable object cannot be owned (because if the owner is not exposed, then the immutable object’s “ever peer consistent” characteristic would be violated). There is no need to own an immutable object, however, since the reason to own an object is to control when it is peer consistent, and immutable objects are always peer consistent.

(There are three other restrictions associated with @Immutable@. They are: a constructor of an @Immutable@ class must end by calling its base class constructor; a class is allowed to be declared @Immutable@ only if its base class also is @Immutable@ or is System.Object; a class or interface that derives from an @Immutable@ type must also be declared to be @Immutable@.)

Coming back to pure methods, note that an @Immutable@ class can invoke pure methods (but only pure methods) on its representation objects. This is possible because the immutable object (the owner in this case) does not need to be exposed (good thing, since one is never allowed to expose an immutable object) in order to invoke a method on the @Rep@ field.

It gets hairier: subclasses and additive

In the above, we have talked about an object being exposed. Let us now be more precise. What is exposed is not the entire object, but a class frame of the object. For example, consider an object of a class C, which is a subclass of B, which is a subclass of A, which is a subclass of System.Object. That object can be exposed for class frame C, for class frame B, or for class frame A (but not for System.Object, which we happen to disallow). If the object is not exposed for any class frame, then it is “fully valid”. Similarly, to be more precise about owners, an “owner” is not just an object, but an (object, class frame) pair.

When you expose an object, you expose it at a particular class frame. The static type of the expression to be exposed by an expose statement is what indicates what class frame to expose. You are only allowed to expose one class frame of an object at a time. When an object is exposed for a particular class frame, then fields declared in that class frame are allowed to be updated. When the end of the expose statement is reached, the object invariant declared in the indicated class frame is checked.

Sometimes it happens that an object invariant in a class C introduces a constraint between a field declared in class C and a field declared in a base class B. In such cases, it would be necessary to check the invariant at the end of expose statements for the B class frame. But this code (in class B itself, say) that uses an expose statement for frame B of an object might not be aware of class C, which makes it problematical to modularly verify class B—if one ignores the possibility of subclasses like C, then one would end up with an object that, after the expose statement, is “consistent” yet its invariant does not hold (violating a vital property of Spec#); if one instead admits the possibility that there may be a subclass, yet unknown, with an object invariant that mentions the fields declared in B, then the verifier would have little choice but to report a possible invariant violation of an unknown invariant.

In Spec#, an object invariant is allowed to mention a mutable field of a base class only if the field has been marked with @Additive@. The notion of “additive” means that subclasses are allowed to add further constraints on the value of the field. In order to assign to an @Additive@ field declared in a class B, the target object must be exposed for frame B as well as the frames of all of B’s subclasses. This is accomplished by the use of an @additive expose@ statement (which syntactically is like an @expose@ statement, but with the keyword @additive@ in front).

The precondition of additively exposing an object at a class frame B is that all subclass frames of the object have already been additively exposed. This means that a program needs to start by doing an additive expose of the most derived class frame of an object, that is, the class frame corresponding to the allocated type (aka the dynamic type) of an object. Then, the program would do an additive expose on the next most derived class frame of the object, and so on, until it performs an additive expose for B. Since in an object-oriented program, the allocated type of an object is generally not known, these additive expose statements are best placed in the respective overrides of a virtual method. To get the appropriate precondition for such a virtual method, mark it with the attribute @Additive@. This makes the precondition of the method override in each class D “object @this@ is additively exposed for all class frame in subclasses of D, but the class frames of D and its base classes are not exposed”. Consequently, at the call site where the dynamic dispatch of the method takes place, the precondition is thus that the receiver object is consistent. As another consequent, a method override that calls its base-class implementation must first additively expose the object, as in:

		    override void M() { additive expose (this) { … base.M(); … } }
	

where @M@ is a virtual method marked as @Additive@. A class should always override all of its inherited @Additive@ methods, possibly with the code shown here for M without the two ellipses (this check is not present in Spec#; our plan is to have the compiler insert this code if the programmer omits the override, but this has not been implemented). It is worth noting that a non-Additive virtual method that calls @base.M()@ needs to do so outside any expose statement.

Suppose the body of an @Additive@ virtual method @M@ wants to call a non-virtual method @N@ in the class to perform some of the work. If @M@ calls @N@ outside any of its additive expose statements, then mark the non-virtual method @N@ with @Additive@ to get the appropriate precondition. If @M@ calls @N@ from inside an additive expose statement, mark @N@ with @Inside@ @Additive@ to get the appropriate precondition. (Although probably much less common, you can declare any parameter whose static type is a class @T@ with @Additive@. This says that the parameter is in a state where one can additively expose it for class frame @T@.) It is not possible for an @Additive@ virtual method @M@ to call another virtual method, @Additive@ or not—the precondition of the call would not work out.

It is possible to (non-additively) expose a class frame @D@ of an object while some number of other class frames are additively exposed, as long as the @D@ is not additively exposed. As stated above, we only support (non-additively) exposing one class frame at a time for an object.

Final words

If you have a situation that is not described above, your solution may be to mark the method with @NoDefaultContract@. This disables the defaults. You can then write some of these specifications manually. For example, for any expression e of a reference type, you can write @e.IsConsistent@ and @e.IsPeerConsistent@. There are some other things you can write, too, like @e.IsExposable@, but we’re hoping that there won’t be any need for such. We don’t provide ways in the Spec# syntax to express every imaginable property about our object model. If your needs exceed what has been described here, we’d be interested in hearing about your programming situation so that we may think of adding support for it.

Rustan Leino