The (near) future of Code Correctness

Posted by Patrick Smacchia on November 6, 2008

I just
watched this amazing PDC presentation (the most impressing I saw so far):
Contract Checking and Automated Test Generation with Pex by Nikolai Tillman and
Mike Barnett.

 

 

 

It is
talking about .NET 4 support and tooling around contracts. I strongly encourage
you to take an hour to watch it. .NET 4 will come with a contract API, System.Diagnostics.Contracts,
much more compelling than the simple (yet very useful)
System.Diagnostics.Debug.Assert(…). What is not said (unless I missed it?!) is
if there will be some tooling to transform automatically existing Debug.Assert(…)
within the new contract API calls. I hope so! The code base of NDepend contains currently 3 470 calls
to Debug.Assert(..) for 69 256 lines of code.

 

I take a
chance here to praise the usefulness of contracts and more specifically of
Debug.Assert(…). I always felt that there is too much emphasis in the community
on automatic testing compare to contracts. For me, these 2 correctness
techniques are equally efficient. And actually, what the presentation shows
well thanks to the super-promising Pex tool,
is that automatic testing and contracts are 2 sides of a same discipline that
consists in finding code defects automatically. Pex will promote contract
amongst automatic test addict developers and that is a good thing. As a side
note, I explained in a previous post why and how Debug.Assert(…) checking must
be activated during automatic tests run.Unit Test vs. Debug.Assert() 

 

My feeling
has always been that automatic tests
and the code itself are 2 different
ways to express the same thing: how a piece of code should behave. Code tells
the machine how to do it, step by step
(do this to compute result from an input) while automatic tests represent a more declarative
way of saying what the code should do (this result must be
computed from this input), what can be seen as specification. Generating automatically tests from code, this
is the job of Pex, makes sense because as just said, the code already
contains enough information needed to test it. There is a problem however: if
the code contains some behavior defects, Pex will generate flawed specification.
This is why contract are needed, to assert specifications that cannot be inferred
from the code and see if the code abides by the contracts rules.

Bets are open:
C#5 will come with some syntax sugar that will generate IL code that will call the .NET 4 contract API under the hood, a bit like the using {…} syntax sugar calls the IDisposable API.

 

 

This entry was posted in Uncategorized. Bookmark the permalink. Follow any comments here with the RSS feed for this post.
  • MS

    Hello Patrick,

    please don’t take me wrong – I don’t want to stop you from being enthusiastic about the features .NET 4 might bring.
    My hope is you attended the appropriate seminars at the university. There you should have taught that defect free programs cannot be proven and thus you can never seriously claim [for any advanced program] that it were defect free.
    Anyway, maybe .NET 4.0 will counter-proof a long known cs’ fact. I will be happy to see this happen.

  • Jim Cooper

    “There is a problem however: if the code contains some behavior defects, Pex will generate flawed specification.”

    It’s a general problem with doing things that way round.

    There’s not really any point generating tests to prove that the code you wrote does what it says it will (unless you’re a compiler writer, I suppose). It much more useful to have tests to determine if it does what you **intended** it to do. I remain unconvinced this is particularly susceptible to automation.

    Now, a tool that generated code from your tests, that’d be interesting :-)

  • Stephen

    I just think theres some obvious ‘hacks’ happening where the concept doesn’t fit 100% in as a library, they’ve done great work arounds but I’d love to see it become more formal to the language.. places like invariants and interfaces where you need to write a private impl or specifically marked member. Surely at least they would support the ! syntax, since they consider ‘nullability’ expressions a flaw in the language..

  • http://wekempf.spaces.live.com wekempf

    I think Stephen meant C# 5, not 4. I’d expect some syntactic sugar for this stuff in 5 as well, though it’s not critical. After all, the sugar wouldn’t add any functionality we don’t get with System.Diagnostics.Contracts, it would just make the syntax easier to write (and arguably, harder to read).

    // Today
    void Foo(string bar)
    {
    Contract.Require(bar != null);
    Contract.Require(bar.Length > 8);
    // …
    }

    // Theoretical syntactic sugar
    void Foo(string! bar)
    require bar.Length > 8
    {
    // …
    }

    The nonnullable type certainly is easier to type, but until you know what the ‘!’ syntax does, it’s less readable. Language support for requires/ensures doesn’t add that much benefit to coding, but also doesn’t lose any readability. I like the sugar, but it’s certainly not necessary… so who knows, maybe we’ll never get the sugar.

  • http://www.NDepend.com Patrick Smacchia

    Stephen, be VERY surprised, the contract won’t meet C#4 :o(
    http://code.msdn.microsoft.com/Project/Download/FileDownload.aspx?ProjectName=csharpfuture&DownloadId=3550

    This is something I asked personally for a long time to the C# team (I am an MVP C#) but without any success.
    http://codebetter.com/blogs/patricksmacchia/archive/2007/07/25/i-want-non-nullable-types-in-c-4.aspx

    Andres Hejlsberg publicly admitted recently that the lack of non-nullable type in C# is their biggest mistake:
    http://www.computerworld.com.au/index.php/id;1149786074;pp;3;fp;;fpid;
    I just don’t understand why they just don’t add this feature at language level??!

    wekempf, I completely agree with you, I feel much more excited by this contract announcement than by the new C#4 featur(ette)s. On the other hand it is not a bad thing C#4 delta with C#3 is so small. It will let more time for the community to master LINQ.

    The fact is that most developers are not aware of contract usefulness, and they blindingly follow the language innovation. Hopefully MS engineers are smart and there is no doubt for me that they took the decision to promote seriously DbC with .NET 4.

  • http://wekempf.spaces.live.com wekempf

    One of the coolest things about this, is you can use it today with VS2008 and VS2005. Unlike Spec#, this uses code instead of attributes, and then post processes the IL (so it works with every language/compiler with no changes) to ensure proper DbC (inheritance rules, etc.). Wicked cool.

    BTW, I think DbC is much more important than testing. It “scales” better, as the contract is codified and checkable not only at the source, but also at the consumers. IOW, if I have a method Foo() which takes an integer that must be within some range, it’s easy enough to write a test for Foo(). It’s much more complicated, however, to write proper tests for Bar() which calls Foo(), or Baz() which calls Bar(). However, with DbC you get compile time AND runtime checks on things like this. Add static analysis tools like Plex, and you also get auto-generated test cases. Just as important, we now get proper documentation for our APIs!

    I wrote a blog about this on my companies intranet. This is as big, if not bigger, than the other announcements about the next version of C#/.NET. I can’t believe it’s not gotten the attention it deserves, in comparison to “dynamic”, variance and optional/named parameters. I meant to publicly blog about this as well, but haven’t found the time yet, but I’m glad to see someone else doing it.

  • Stephen

    I would be VERY suprised if the next iteration of C# didn’t have a cleaner built in ‘spec# like’ syntax for doing contracts..