As Nick pointed out in response to my previous post, the syntax I baked up for DbCiC (”Deb Kick”, clever eh?) is fairly poor. Not only is it ugly, but expressing pre-/post-conditions pertaining to things other than return values and parameters - a fairly common case - is not very trivial to acheive. (Hey, I was tired!)

I am leaning towards the following BNF (left-recursive) grammar:

<Contract> : <RequireClauses> <EnsureClauses>

<RequireClauses> : nil | requires <RequireClause>

<RequireClause> : <BooleanStmt> | <RequireClause>, <BooleanStmt>

<EnsureClauses> : nil | ensures <EnsureClause>

<EnsureClause> : <BooleanStmt> | <EnsureClause>, <BooleanStmt>

My example from my previous post would look like this:

  int divide(int a, int b)

    requires b != 0

    ensures [return] == a / b

  {

    return a / b;

  }

Yes, I did shamelessly pilfer Eiffel's keywords as I find that they are clear, unambiguous and improve readability. It is slightly more verbose, but this is a GoodThing(tm) IMHO.

At this point, I have a pre-compilation app that simply parses and expands the tokens into the desired result (almost done, code will be posted once it's 100%); I am also playing with an extension to the (Rotor) C# compiler, but there's something attractive about having this decoupled from the actual compiler implementation. Source line #-to-IL mapping for debug purposes would be challenging without compiler support, however, necessitating some post-csc IL/PDB patching to remap lines back to the original source.