More on Specifications

4/1/2006 10:08:45 AM

More on Specifications

In my previous post on specifications,  there were some comments raised on the three approaches to adding requirements.

My tool doesn’t require modification of code. The utility of a utility is increased when no action is required of the utilizer. However, I will allow developers to add additional information.

Omer suggested a fourth option of somehow including specifications with XML comments. This could involve either creating a new tag that may not be picked up by existing documentation generators, or by recognizing a <span> tag with a class attribute around an expression.

The C# compiler already provides the option of collecting XML comments into a single XML file. NStatic could possibly do the same, adding both implicitly generated and explicitly entered specifications to the mix. Other interesting ideas include automatic translation of expressions into natural language.

With regards to run-time checks, it should be possible for NStatic to recreate an existing project with dynamic runtime checks automatically inserted.

I looked at preconditions, but what about other phenomena possible in Spec#.

In these other cases, the third approach of using actual code “MyClass.Requires(constraint)” loses out to comments and attributes. Class-based invariants requires a separate function to house the invariants and repeated code insertions at the start and end of every public method body. Postconditions may require entire method blocks to be wrapped in a try-finally clause. Interface invariants, pre– & post– conditions can’t even use code insertion.

Commented constraints are more readable than attributed constraints, but are not accessible via reflection. Attributes are not composable, so the syntax becomes awkward in certain situations where, for example, a checked exception includes a postcondition, which may itself throw its own exception.

Non-null Fields, Parameters, and Return Types

class Student : Person {
    [NonNull] Transcript t ;


Pre & Post-conditions

With regards to run-time checks, it should be possible for NStatic to recreate an existing project with dynamic runtime checks automatically inserted.

class ArrayList {
void Insert(int index , object value)
requires 0 <= index && index <= Count
otherwise ArgumentOutOfRangeException;
requires !IsReadOnly && !IsFixedSize
otherwise NotSupportedException;
ensures Count == old(Count) + 1;
ensures value == this[index ];
ensures Forall{int i in 0 : index ; old(this[i]) == this[i]};
ensures Forall{int i in index : old(Count); old(this[i]) == this[i + 1]};

Alternatively, alternatively using attributes we could write in a somewhat less readable way.

[Requires(“0 <= index && index <= Count”, ArgumentOutOfRangeException”)]
[Requires(“!IsReadOnly && !IsFixedSize”, “NotSupportedException”)]
[Ensures(“Count == old(Count) + 1”)]
[Ensures(“value == this[index ]”)]
[Ensures(“Forall{int i in 0 : index ; old(this[i]) == this[i]}”)]
[Ensures(“Forall{int i in index : old(Count); old(this[i]) == this[i + 1]}”)]   
void Insert(int index , object value)

Checked Exceptions

char Read()
throws SocketClosedException;

void ReadToken(ArrayList a)
throws EndOfFileException ensures a.Count == old(a.Count);

Interface Constraints

interface I
        void M(int x )
            //! requires x <= 10;

I actually do have another approach using my rule language based on pattern-matching, but meant for broad classes of errors.







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