Specifications

3/31/2006 5:41:21 PM

Specifications

Spec# is an experimental specifications-base version of the C# programming language designed by Microsoft Research. Previous languages like Eiffel included specifications, which were converted to run-time checks. Spec# includes an automatic program verifier called Boogie that checks specifications statically.

NStatic is similar to Spec# cum Boogie in its capabilities; I do not know whose engine is richer. It is different in that specifications in Spec# are explicit, while those used by NStatic are automatically inferred from the code itself. Inferred specs can be view from the NStatic user interface. 

Although implicit, NStatic already has the ability to work with specifications, and the natural next step is to allow the user to create explicit specifications. To some extent, this can already be done by using Assert function calls.

While it’s a small task for me to modify my C# parser to read in explicit specifications, I’ll probably wait until version 1.5. (All versions 1.X to 2.X will be available as a free upgrade to 1.0, since I don’t have a quality assurance team that can test with usage patterns different from my own.)

I been looking into reusing some of the syntax from Spec# such as requirements, invariants, and checked exceptions. Non-null types would also be supported either through a NonNull attribute or a fully written out requirements clause.

This is what a requirements clause looks like in Spec#.

class ArrayList {
public virtual void Insert(int index , object value)
requires 0 <= index && index <= Count;
requires !IsReadOnly && !IsFixedSize;

I have been thinking about three different forms of adding requirements to code being fed through NStatic. I am thinking of accepting all three as mutually inclusive, alternate ways of adding requirements.

1) The first approach is to enable escaping into Spec# mode through the use of a comment. (//!) When viewed from with the NStatic text editor, special syntax highlighting would be enabled to highlight and syntax check the escaped code.

public virtual void Insert(int index , object value)
//! requires
0 <= index && index <= Count;
//! requires
!IsReadOnly && !IsFixedSize;

2) The second approach is to recognize any user-defined attribute with the name RequiresAttribute, so code could alternatively be written as the following and available through Reflection. The use of Reflection allows specifications to be easily extracted for documentation.

[Requires(“0 <= index && index <= Count”)]
[Requires(“
!IsReadOnly && !IsFixedSize”)]
public virtual void Insert(int index , object value)

The RequiresAttribute must be defined by the developer as no libraries will be available to reference from. Using the Conditional(“DEBUG”) attribute on the RequiresAttribute will eliminate the overhead from the release build. (I’ll likely include a sample source file that anyone can include in his project.)

3) A third approach involves the recognition of special function calls, similar to how NStatic currently special-cases any method call involving the method name Assert and Fail, regardless of the class.

public virtual void Insert(int index , object value)
{
     MyClass.Requires(0 <= index && index <= Count);
     MyClass.Requires(
!IsReadOnly && !IsFixedSize);

The advantage of this approach over the other two is the ability to perform runtime-checks.

The first approach using comments is perhaps redundant, so I may not ultimately use it. I’ll write more about specifications and my rule language later.

Comments

 

Navigation

Categories

About

Net Undocumented is a blog about the internals of .NET including Xamarin implementations. Other topics include managed and web languages (C#, C++, Javascript), computer science theory, software engineering and software entrepreneurship.

Social Media