Summary: a quick summary of the SpecSharp attributes
Nearby: FrequentlyAskedQuestions

Namespace: Microsoft.Contracts
Assembly: System.Compiler.Runtime (in System.Compiler.Runtime.dll)
Version: 1.0.6526

General note

Many of the attributes listed below are used to encode language level constructs from Spec# into MSIL (e.g., Ensures, Throws, etc.). As such, only some of the attributes are expected to be used by programmers directly. We should group them into two categories, internal and public attributes. Internal attributes are expected to change without notice.

AtributeWithContext

Undocumented

Captured

Undocumented

Confined

The Confined attribute claims that the method on which it appears has no observable side effects and additionally that it does not depend on any non-StrictReadonly static or instance fields other than the instance fields of the receiver object and its transitively owned objects. Methods used in object invariants must be marked Confined.

Delayed

(see NotDelayed)

Does

Undocumented

EncodedTypeSpec

Undocumented

Ensures

The Ensures attribute is used by the compiler to encode method postconditions in the binary assembly so that they can be picked up by downstream analysis tools (i.e., Boogie). It is not meant for users at the Spec# source level.

Immutable

Undocumented

Invariant

The Invariant attribute is used by the compiler to encode object invariants in the binary assembly so that they can be picked up by downstream analysis tools (i.e., Boogie). It is not meant for users at the Spec# source level.

LockProtexted

Undocumented

Modifies

The Modifies attribute is used by the compiler to encode method modifies clauses (lists of what the method is allowed to change in the heap) in the binary assembly so that they can be picked up by downstream analysis tools (i.e., Boogie). It is not meant for users at the Spec# source level.

MustOverride

The MustOverride attribute is used on virtual methods to indicate that all further concrete subclasses must also implement (override) the method. The subclass implementation must also be annotated with the attribute. Abstract classes do not have to implement methods annotated with this attribute, but if they do, then they must mark the override with the attribute. If they define any new methods, then they should be annotated if subclasses are supposed to define an override. A method that was not originally annotated with the attribute can have an override that is annotated with it; the annotation is then binding upon further subtypes.

NoDefaultActivity

Deprecated. Please use the NoDefaultContract attribute instead.

NoDefaultContract

The NoDefaultContract attribute instructs the compiler not to add any of the normal default preconditions to the method. (In order to reduce the annotation burden on programmers, a number of pre conditions and post conditions are automatically added to every method. For example, without the NoDefaultContract attribute a method will have a pre condition that requires its object to be in state where the invariants hold.)

NotDelayed

We also have come up with a new way to handle the problem of base constructor calls and non-null fields. By default we consider all constructors to be “delayed”. Such constructors assign to fields of “this”, but never read from such fields. Delayed constructors do not need to explicitly call the base constructor after initializing non-null fields. To indicate that a constructor is not delayed, use the NotDelayed attribute on it.

NotNull

Undocumented

NotNullGenericArguments

Undocumented

Owned

Undocumented

Pure

The Pure attribute claims that the method on which it appears has no observable side effects. This attribute is typically applied to methods that are called from inside pre and post conditions. (It is important that pre and post conditions have no observable side effects.)

Reader

Undocumented

Requires

The Requires attribute is used by the compiler to encode method preconditions in the binary assembly so that they can be picked up by downstream analysis tools (i.e., Boogie). It is not meant for users at the Spec# source level.

RequiresCanWrite

Undocumented

RequiresImmutable

Undocumented

RequiresLockProtected

Undocumented

ShadowsAssembly

The ShadowsAssembly attribute is an assembly-level attribute that is put in an out-of-band contract to point to the assembly that the contracts are meant for. It is put into an assembly automatically by the Visual Studio integration by setting the "Original assembly" property in the General pane fo the project properties of a Spec# project. If you do not use Visual Studio, you may place this attribute on the assembly manually: ShadowsAssembly('''''<path to shadowed assembly>'''''.

SkipVerification

Deprecated. Please use the Verify attribute instead.

SpecInternal

Undocumented

SpecProtected

Undocumented

SpecPublic

In some cases, an instance variable might have been marked private just to prevent public clients from updating it. In that case, you still want the public client to know about the field. And if that's the case, you can mark your field with the SpecPublic attribute, which allows you to mention the field in specifications as if the field had been public.

StateIndependent

The StateIndependent attribute claims that the method on which it appears has no observable side effects and additionally that it does not depend on any non-StrictReadonly static or instance fields.

StrictReadonly

The StrictReadonly attribute may be applied only to readonly instance fields. Contrary to readonly fields in general, StrictReadonly fields may be assigned to only once. They must be initialized before the base class constructor is called. The Spec# program verifier knows that StrictReadonly fields never change.

Throws

Undocumented

Verify

The Verify attribute determines whether or not the static verification should attempt to verify a method or not. The absence of the attribute is taken to mean that the method should be verified. The attribute is searched for first on the method, then on its declaring type, and then on the declaring assembly. So to shut off verification for the entire assembly, place Verify(false) on that level and then to turn it on for a particular class (type), you can put Verify(true) (or simply Verify since the nullary constructor defaults to true) on it. And then you can turn it off again for a particular method in the class by putting the attribute back on that method.

Writable

Undocumented