PostSharp

[soren]

I've done a few initial attempts to make a method contract framework using Laos. It's extremely simple:

    [Contract]
    public class SomeClass
    {
        [return: NotNull]
        public string SomeMethod([NotNull] string input)
        {
        ...
        }
    }

Laos injects runtime checks into using a MethodBoundaryAspect.

And that's basically how far I got. To call this a complete specification framework, it would need to enable you to do the following:

Specify pre- and post requirements ([b]requires[/b] and [b]ensures [/b]in spec#) that are more complex than simple NotNull requirement
Specify invariants (in the form of Lambda expressions?)
Maybe automatically perform some kind of static theorem analysis?

I believe I've reached the limits of what can be done with Laos. And I haven't dived into the low level codeweaver yet.

What do you think? Can CodeSharp make it work, and if so, what's the effort involved?

/Soren

[gfraiteur]

This is not the scope of Laos. Of course there are things you can perform, but you will pay a too big price in performance.

Ideally one should use the low-level API to emit optimized instructions.

The problem with specifying complex invariants to how to integrate them in the C# syntax. You cannot specify lambda expressions in a custom attribute, for instance. But you can add a method and decorate it with an [Invariant] custom attribute:

class MyClass
{
int a, b;

[Invariant]
bool CheckInvariant()
{
return a + b < 10;
}

public void SomeMethod()
{
a++;
b+=a;
}
}

PostSharp could invoke CheckInvariant after "SomeMethod()" and even do more complex things (like avoiding to check invariants when the class is calling itself).

Performing static analytis is still more difficult. It will be for a next step. Actually I think it makes sense to implement some simple analysis (null, dispose, ...), but one should be careful. Should correctness validation be done at MSIL level? Isn't it better to do it at source level? The success of some source code checkers like Resharper suggest that one should perform source-level analysis when possible. Which makes sense: one should always validate first the most abstract model.

As for the work estimate: doing a validation framework without static analysis is a matter of weeks to prototype. With static analysis, a matter of months.

[soren]

Good points, Gael.
I know there's a price for runtime checks. I think sometimes the price is valid, because raising exceptions early is better than debugging for a long time looking for derived errors elsewhere in your code.
I hadn't thought of putting invariants inside a method and then applying those as aspects. While it's pretty and readable, there are two downsides: 1. There's no communicating to users of your code which invariants, requirements or "ensure-statements" apply to which methods. 2. The invariant method can only access fields, not variables local to - in your example - SomeMethod().
I tried moving away from aop and made a class called Invariant that allows me to do this:
public void SomeMethod(int i)
{
    using(Invariant.SpecifyThat(() => i < 10)
    {
        ....
    }
}

It's dead simple, uses IDisposable to ensure the lambda expression is invoked both before and after the code block. The SpecifyThat static method simply takes an argument of type Func<bool>.
It's not pretty but it's not as ugly as it would be before C# 3.0.
As for static analysis, it's dead complicated and I'm not convinced it's worth the effort. So I guess I'm satisfied with a few parameter checks and invariants for now.
Regs,
Søren

[mihies]

Previously Soren Skovsboll wrote:

I believe I've reached the limits of what can be done with Laos. And I haven't dived into the low level codeweaver yet.

/Soren

Do you mind posting your code so I don't have to reproduce it? I would like to test for null/not null values right now. I don't mind performance issues since I'll be using it for debug purposes only.

Thanks

[cocotapioca]

Yesteday i got the NonNull attribute for parameters using PostSharp for emitting IL code.

[blahetal]

hey guys, can you share your code. I`d like to use some simple pre- and post-conditions in my project.

idea - what about making a new PostSharp plugin - PostSharp4DbC (design by contract) or something like that

[cocotapioca]

I zip some code at:
http://rapidshare.com/files/97525457/Projects.zip.html

Im planning to make a plugin of this but am lazy.
Id appreciate comments.
Cheers.
Ignacio.

[soren]

Sure, here's some work in progress:

http://www.skarpt.dk/DbcUsingAop.zip

Let me know if you need further usage info.

Regs,
Soren

[blahetal]

thanks, your code is pretty hardcore . I will need some time to go through it

[gfraiteur]

Hi mates,

I've briefly looked at your codes. Soren uses Laos, Ignacio is quite brave and uses Core...

Ignacio's approach is maybe the one providing correct performance. Using Laos to check that a field is not assigned to null seems a big performance overhead, even if in some scenarios performance of .NET code just does not matter. Most frequent conditions, like non-null, should indeed generate ad-hoc code.

I do think that Laos, in its current version, is not the right tool for DbC. The reason is performance: Laos generates code to invoke handlers you don't even implement; Laos is purely loosely types, which provokes a lot of boxing and type casting.

I think the right answer is that I should provide the features so that people can build easily their DbC with the required level of performance. I still don't know exactly how to realize this, but it is very high on my list of priorities.

Another missing feature is contract inheritance (method implementations should respect the contract defined on the abstract method definition). That's also something that is not possible to achieve with Laos.

As you can see, there is a lot of work! And it will not be for tomorrow.

Guys, what I can propose you is to host your code on the project http://code.google.com/p/postsharp-user-plugins/. If you are wanting to release your code under a reasonable open-source license, it is maybe the best way to maintain the project. I guarantee many people will be interested.

Thanks again for your good work!

Gael