Specifications

10/5/2007 4:51:05 PM

Specifications

My main tasks in the past couple of months have been divided between bug-fixing and improving scalability. In the latter case, testing on large projects revealed bottlenecks caused by uncontrolled expression growth, for which I came up with a general solution. I have been spending a considerable amount of time on my simplifier for recursive lambda expressions.

There was one major addition. I added syntax support and highlighting for eventual specification support. My immediate goal was to provide a clean way of adding breakpoints and assertions to the source code.

image

The above visual shows what the new syntax highlighting looks like. The new keywords are bolded. Two new grayed out comment delimiters were added: //@ and /*@. These comment delimiters act like white space from within NStatic with the exception that new keywords are only recognized within the comments.

Any arbitrary code, such as ghost fields, can be placed inside these comments; this serves as an alternative to using the preprocessor defines, NSTATIC and CODEANALYSIS.

The new keywords that I have included: require, ensure, assert, assume, pure, modifies, invariant, old, breakpoint, result, unreachable, and nonnull. But, for the first release, the only keywords that are actually effective are assert, assume, breakpoint, old. Assert actually verifies that the expression is true and returns a warning otherwise (or error in the case of an invalid code path). The behavior is stronger than a call to Debug.Assert. Assume does not require the expression reduce directly to a true value, but it will produce a error if there is a false path leading to it.

The specifications are modeled on both Java Modeling Language (JML) and Spec#. There are quite a number of differences between the two. For instance, JML incorporates method contracts before the method declaration whereas Spec# incorporates contracts just right before the method block. While I followed the Spec# in this case, my instinct is to prefer JML, because it is more of an industry standard, and I am less likely to encounter Microsoft IP issues.

I suspect highly that the next version of C# will incorporate some kind of design by contract.

There are a few differences from both JML and Spec#.

  • Arbitrary functions are supported as expressions with specifications, including impure functions (functions containing side-effects). Side effects that occur inside the expression of a single specification are not visible to other parts of the program, including adjacent specifications.

I have never taken a course in formal methods, so I am not fully aware of the implications of my approach.

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