Any alternatives to the .Net 4 Code Contracts static analyser?

views:

342

answers:

+6 Q:

Any alternatives to the .Net 4 Code Contracts static analyser?

It seems that the static analyser for use with the .NET 4.0 Code Contracts is only going to be available for Team Suite editions of Visual Studio - this puts it well outside the budget for my team.

Are there any alternatives (open source, free or reasonably priced) which offer similar static analysis for design by contract style code (not necessarily using .net code contracts). I'm guessing the answer will be no as the full worth only comes when the BCL itself has contracts - but are there any which go part of the way?

+2 A:

I'm not sure if that's what you are looking for, but you may have a look at Frama-C and its ACSL annotation language for C.

Compared to .NET contracts, ACSL contracts are not executable (it's impossible to check them with run-time assertions) but are better suited to static analysis (they are more expressive and allow a full specification to be written and statically checked. At least theoretically)

Pascal Cuoq 2009-10-31 19:51:35

At a quick glance that looks really impressive - especially with all the plugins. The value analysis plugin in particular is amongst the things I'd like to use. I'll definitely check it out! I see that it's a generic toolset for anything in the C family - any experience of how it fits in with C# or common pitfalls to avoid?

FinnNk 2009-10-31 21:30:25

@FinnNk I am not sure about "anything in the C family"... It's only for C. The initial effort was towards handling critical embedded C, so the problem of interfacing C# or other languages with their own syntax for contracts has been completely ignored. And since there is still a lot happening on the .NET contracts side too, it would still be a little bit premature right now, although that sounds like an interesting topic.

Pascal Cuoq 2009-10-31 21:39:57

@FinnNk Regarding pitfalls, in the value analysis plug-in, you will quickly find that ACSL support is quite partial (even among the subset of ACSL that can be supported in an automatic, forward-propagation static analysis). As a typical limitation, the value analysis still does not understand \result in post-conditions. Have you seen Jessie's tutorial? It has quite a few complete specifications for simple functions, expressed as contracts. http://frama-c.cea.fr/jessie_tutorial_index.html

Pascal Cuoq 2009-10-31 22:04:28

ansaurus

tags:

views:

answers:

Any alternatives to the .Net 4 Code Contracts static analyser?

related questions