Ants are very fascinating creatures. I've become more appreciative and aware of this recently, as the pages of the following books flowed past my eyeballs:

Emergence: The Connected Lives of Ants, Brains, Cities, and Software by Steven Johnson I bought this several years back (2001, I think), but just picked it up again for a read. It describes the concept of emergence, that is, when given an aggregate, the capabilities (far) surpass the sum of the capabilities of its individual parts. For example, consider ant colonies, in which individual ants are making decisions in isolation based on an extremely limited capacity for analysis and thought. When viewed in the aggregate (colony), however, each ant appears to be contributing to an extremely coordinated, thoughtful, and strategic mass. The author here attempts to be clever on too many ocassions, and the applications to technology are a bit stretched (IMHO). However, it lead me to look deeper into the behavior of ant colonies, and as such was a good “gateway“ read.

Ant Colony Optimization by Marco Dorigo, Thomas Sttzle Read this now. This book focuses on algorithmic techniques for approximation of NP-hard/complete problems, in particular Ant Colony Optimization (ACO). Out of disorder, chaos, and localized decision making, the simulation of ant behavior to attack classic NP-hard algorithms causes fascinating new approaches to problem solving and new approximate solutions to emerge. This is one of the best reads in a while.

As you've most likely already heard, Microsoft announced today that WinFX will target downlevel operating systems (e.g. WinXP and WS03) in addition to Longhorn. This is awesome news. For more details on our plan, I'll leave it to The Man Himself - David Treadwell. Chris Sells also has a great summarization of what this means to WinFX customers.

I'm extremely excited about this... the platform that I live, breath, and... well... y'know... eat, I guess... every day (WinFX, that is) will experience an elevated and accelerated adoption as a result. It'd be awesome if there was a simple switch we could throw that immediately gives everyone LH, but this obviously isn't reality. As a result, shipping on XP and WS03 means that we'll reach a broader audience in a shorter amount of time. ISVs and IT shops can get cooking with gas without requiring that 100% of their users be on the “latest and greatest” OS. Goodness if you ask me.

Update: Soma offers up some perspective, and Paul Thurrott gives some historical insights and opinions as to why this is a good move for the big house.

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.

You just have to love the age of ubiquitous, blazingly quick Internet access. Virtual information at your fingertips...

>ping -t www.bluebytesoftware.com
Reply from 209.35.183.214: bytes=32 time=78ms TTL=48
Reply from 209.35.183.214: bytes=32 time=79ms TTL=48
Reply from 209.35.183.214: bytes=32 time=80ms TTL=48
Reply from 209.35.183.214: bytes=32 time=77ms TTL=48
Reply from 209.35.183.214: bytes=32 time=82ms TTL=48
Reply from 209.35.183.214: bytes=32 time=77ms TTL=48
Reply from 209.35.183.214: bytes=32 time=93ms TTL=48
Reply from 209.35.183.214: bytes=32 time=79ms TTL=48
Reply from 209.35.183.214: bytes=32 time=79ms TTL=48
Request timed out.
Request timed out.
Reply from 209.35.183.214: bytes=32 time=78ms TTL=48
Reply from 209.35.183.214: bytes=32 time=84ms TTL=48
Reply from 209.35.183.214: bytes=32 time=79ms TTL=48
Request timed out.
Request timed out.
Request timed out.
Reply from 209.35.183.214: bytes=32 time=80ms TTL=48
Reply from 209.35.183.214: bytes=32 time=79ms TTL=48
Reply from 209.35.183.214: bytes=32 time=92ms TTL=48
Reply from 209.35.183.214: bytes=32 time=77ms TTL=48
Request timed out.
Request timed out.
Reply from 209.35.183.214: bytes=32 time=2173ms TTL=48
Reply from 209.35.183.214: bytes=32 time=80ms TTL=48
Reply from 209.35.183.214: bytes=32 time=77ms TTL=48
Request timed out.
Request timed out.
Reply from 209.35.183.214: bytes=32 time=77ms TTL=48
Reply from 209.35.183.214: bytes=32 time=77ms TTL=48
Reply from 209.35.183.214: bytes=32 time=81ms TTL=48
Reply from 209.35.183.214: bytes=32 time=94ms TTL=48
Request timed out.
Reply from 209.35.183.214: bytes=32 time=159ms TTL=48
Reply from 209.35.183.214: bytes=32 time=80ms TTL=48
Reply from 209.35.183.214: bytes=32 time=88ms TTL=48
Reply from 209.35.183.214: bytes=32 time=345ms TTL=48
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.
Request timed out.

Simply put, contract based programming formalizes the notion of a program’s input/output constraints, supplying first order language constructs to verify and prove correctness. This includes, but is not limited to, the expression of type invariants, pre- and post-conditions, reliability guarantees in the face of unexpected failures, and side-effecting state modifications. For instance, a method which performs division certainly does not want to accept a denominator equal to zero, and an atomic operation producing a return value should always ensure that certain type invariants and consistent state constraints remain true at the end of its execution. Similarly, code which affects the environment in which it executes likely should indicate to callers what to expect should a failure occur; i.e. does an operation make (verifiable) guarantees regarding what actions it will take and succeed at to attempt recovery, or does it simply halt execution and throw an exception? One example of a language which employs such concepts is Eiffel. (I recommend this article for a bit more detail.)

I (along with a number of other people, smarter than myself) assert that supporting such constructs, effectively embedding program correctness checks directly into the runtime, results in a more reliable, stable, and bug-free execution environment. With most mainstream programming languages lacking such support, proofs and verifications are encoded in manual if(x){throw;} statements, and proving correctness (hopefully!) captured in hand-crafted unit tests. Unfortunately, this significantly hampers readability, writability, and prevents any structured way to discover an operation’s implicit contract, leaving brute force poor-man’s-proofs to perform a critical job. In fact, testing as we know it changes dramatically with contract based programming, essentially becoming an exercise in validating that the appropriate contract guarantees have been put in place; the proof part is taken care of by the execution environment.

While I’ve certainly not completed the thought process here, I wanted to walk through some random ideas I have on the subject. To be entirely transparent, my goal here is to add support to the C# language.

Language Support

Type invariants can easily be supported by requiring types to implement a specific interface, for instance:

  interface IContract

  {

    bool Invariant();

  }

Specifically, however, my primary focus will be on pre- and post-conditions, leaving the more difficult reliability and side effect support off the table for now. Additionally, I explicitly wanted to avoid mandating developers to sprinkle asserts throughout the main bodies of their code. (There are already frameworks out there that work in a similar fashion, and indeed System.Diagnostics.Debug.Assert() is a handy tool for this job.) Because we have not yet devised a means by which to express these constructs in code yet, the discussion will feel a bit loose to begin with. Hopefully it comes together as my brain dump progresses…

Given the method:

  int divide(int a, int b)

  {

    return a / b;

  }

And its pre-condition: b != 0 and post-condition: returnValue == a / b, for example.

The following pseudo-code represents one possible version of the desired automatic expansion. (Note that the question of what specific assembly image (debug vs. release, etc.), whether these checks occur at the call site or not, etc. are all interesting questions I will consider below in the Runtime Verification section. This section simply considers how to enable these expressions in the C# language.)

  int divide(int a, int b)

  {

    assert(b != 0);

    int z = a / b;

    assert(z == a / b);

    return z;

  }

More generally and accurately, an expanded operation should look something like this, ensuring an assignment to returnValue wherever the pre-expanded method body returns just prior to doing so:

  T[...] operation(T a[...], ...)

  {

    // pre-condition asserts

    T returnValue;

    bool caughtFailure;

    try

    {

      // method body

    }

    catch

    {

      caughtFailure = true;

      throw;

    }

    finally

    {

      if (caughtFailure)

        // reliability asserts

      else

        // post-condition asserts

    }

  }

My initial approach was to consider using attributes. For example:

  [PreCondition("b != 0")]

  [PostCondition("returnValue == a / b")]

  int divide(int a, int b)

  {

    return a / b;

  }

This was attractive due to the reuse of an existing language feature, however was quickly discarded for a number of reasons. First, expressing constraints this way is an extraordinarily unnatural thing to do, especially given the context and scope to which an attribute has access. The most viable option is to express conditions and the variables to which they apply through very loosely typed means, e.g. strings. Static verification at compile time is challenging with this approach, although probably possible with a large amount of effort. The idea here is that some post-compilation IL-modifier would run, mangling the IL output by the C# compiler, and expanding it into the appropriate code. The attributes disappear from the metadata, and leaves a trace behind only in the form of the expanded pseudo-code above. Perhaps rather than expressing constraints like a mini-scripting language, it could be replaced by simple method references,

  bool Equal(int x, int y)

  {

    return x == y;

  }

  bool NotEqual(int x, int y)

  {

    return x != y;

  }

  [PreCondition("NotEqual(b, 0)")]

  [PostCondition("Equal(returnValue, ???)")]

  int divide(int a, int b)

  {

    return a / b;

  }

But this feels very heavyweight and limited (i.e. you’d need to write a method for each condition; some out of the box ones could be provided, such as IsGreaterThan(x,y) for example, but custom checks would be awkward to create. Additionally, achieving composability seems almost as awkward as the script-like syntax. However, allowing code to be written within strings not only feels too loosely typed, but is really just a hack. This feels like a dead end.

So the next natural step was to consider an extension to the C# grammar. While more complex to implement, it feels like the right way to go about things. The options are endless (well, almost)… however, after a couple minutes of playing around, I’ve become particularly fond of the following syntax,

  int[== a / b] divide(int a, int b[!= 0])

  {

    return a / b;

  }

The code within the brackets implicitly adopts the variable it straddles as its l-value. It isn’t too much of a stretch to envision the code within each bracket either being expanded into the method’s body, or perhaps being pulled out into another operation. This job could be performed by a pre-compiler, and would result in a very statically typed solution. One problem with this approach, however, is that the first class notion of a constraint is lost in the compiled image. No trace is left behind of these checks, removing the possibility of using the data for static consumption; e.g. documentation, call-site verification, etc.

A possible solution is to use a combination of the two approaches outlined above. The attributes could serve as a metadata manifestation of these language constructs. But then we’ve come almost full circle… if attributes are good enough to embed call-site enforcement, then the language support is just superfluous syntactic sugar. Perhaps not. Remember, one of the primary goals is to support better readability and writability, which the language support certainly enables. I think we’ve got a workable solution!

This has the end result of looking as though you'd written the following code:

  [PreCondition("a != 0")]

  [PostCondition("returnValue == a / b")]

  int divide(int a, int b)

  {

    // pre-condition asserts

    assert(a != 0);

    int returnValue;

    bool caughtFailure;

    try

    {

      // method body

      returnValue = a / b;   

    }

    catch

    {

      caughtFailure = true;

      throw;

    }

    finally

    {

      if (!caughtFailure)

        // post-condition asserts

        assert(returnValue == a / b);

    }

  }

Now, just to implement it…
 
Runtime Verification

Some interesting questions arise while considering the implementation. I haven’t thought enough about these problems to surface answers to them all, but nonetheless they are quite interesting.

Done correctly, each operation will probably accumulate quite a few contract constraints, many of which might be expensive to actually execute at runtime. This is perhaps the price you must pay for rock solid, provable reliability, but optimization is not out of the question. A category of checks can probably occur only at compilation time, while another category will execute during runtime. The boundaries of a program are the most obvious pain point on which to focus first. By performing a transitive proof, and if inputs and outputs are guaranteed to be within our expectations, then it makes sense that within our program these constraints must hold true. Mathematic proofs are generally infallible, and this approach uses the same concepts. Thus runtime verification should always occur at any input or output boundary, but it’s also unlikely that this is the extent of it due to such dynamic things as late bound invocations.

Call-site enforcement is also interesting. In many cases, the caller is the one who cares most about having a reliable, correct program. However, cases also exist in which APIs have a significant enough stake in the system as a whole that they would prefer to see such constructs enforced, too, especially when lacking a certain level of trust with the consumer. (Consider core OS APIs, for instance, which most likely would prefer that the system stay in a provable and consistent state at every instant during a program’s execution. For other core OS code which uses it, a given API might just trust that it will do the right thing; however, for applications executing within an Internet-zone, for instance, this is unlikely to remain true.) So it seems that a mixture of call- and called-site enforcement is necessary. Preventing duplicate execution of checks presents a challenge, as does determining exactly what mixture is correct.

There are certainly other considerations to make, such as polymorphic contract constraints, for instance, but I’m too tired to think about them right now. ;)

340hp. 4.2L V8. German engineered.

I love it. And yes, I enjoy frivolous, wallet draining toys.

Breaking changes are typically thought of as modifications which alter a public API's surface area. For example, changing a method name from Foo() to Bar(), or otherwise changing it's signature, such as adding a required parameter. Anything else is simply implementation fodder, subject to change as more efficient and/or appropriate means to compute the same result become available, yes?

Well, not exactly. There are some subtleties. Depending on your perspective, implicit semantic constraints - such as pre- and post-conditions - would likely break existing code if altered behind a client's back. These are slightly less tangible to understand in this context due to the lack of a standard static representation of such notions in mainstream .NET languages. This subtlety is also prevalent with structured exception handling. Consider the following example.

Say there’s a public API defined as such:

  public void DoThrowingOperation()

  {

    throw new CheckExceptionA("Test");

  }

And a client comes along, decides the API’s useful enough to take a dependency on (what, you say, that method's not very useful? bahhh), and adds code which uses it:

  public void DoCheck()

  {

    CheckDepends cd = new CheckDepends();

    try

    {

      cd.DoThrowingOperation();

    }

    catch (CheckExceptionA e)

    {

      Console.WriteLine("Caught exception: " + e);

    }

  }

Well, it's entirely reasonable for them to expect that catching CheckExceptionA is sufficient to recover from specific exceptions occurring from their invocation to DoThrowingOperation(). That is, the only way an exception could leak outside of this method is for a critical system error to occur, or perhaps other exceptions coming from code upon which the public API depends. This is an extremely naive viewpoint, and an obvious reason that clients should properly factor their exception handling code to be resilient against the scenario I describe (e.g. liberal use of finally clauses).

What if the public API changes its implementation vis-à-vis exception throwing patterns? No verification errors here, the API surface area remains the same:

  public void DoThrowingOperation()

  {

    Random r = new Random(0, 1);

    if (r.Next() == 0)

      throw new CheckExceptionB("Ha ha");

    else

      throw new CheckExceptionC("You are broken");

  }

The implementers of the old DoThrowingOperation() thought it made more sense to refactor their exception hierarchy, specifically to separate the errors thrown into two more descriptive classes. Unless these new exceptions derive from the old one (enabling polymorphic catching), however, any clients could be in for a surprise if the new API version is deployed and bound at runtime. The client’s catch clause will never fire now, and in fact any of the new exceptions thrown from this method will propagate freely up the caller’s stack. Boom:

Unhandled Exception: CheckExceptionB: Ha ha
   at CheckDepends.DoThrowingOperation()
   at CheckTest.DoCheck()
   at CheckTest.Main(String[] args)

One could easily rationalize this problem as a result of C#’s lack of checked exceptions. And, of course, one would be wrong in doing so. Checked exceptions, at least in Java’s implementation, are nothing but a compiler trick. Constraints as rich as those necessary to enforce call graph exception checking are much too expensive to verify at runtime, and as such the situation is the same in Java.

For example, this API:

  public void DoThrowingOperation() throws CheckExceptionA

  {

      throw new CheckExceptionA("Test");

  }

And this client code:

  public void DoCheck()

  {

    CheckDepends cd = new CheckDepends();

    try

    {

      cd.DoThrowingOperation();

    }

    catch (CheckExceptionA e)

    {

      System.out.println("Caught exception: " + e);

    }

  }

Wouldn’t play very nicely if the API were altered slightly, even though the API's static throws information has been changed correctly:

  public void DoThrowingOperation() throws CheckExceptionB, CheckExceptionC

  {

    if (Math.random() < 0.5)

      throw new CheckExceptionB("Ha ha");

    else

      throw new CheckExceptionC("You're broken");

  } 

At least in the case of Java, the compiler would catch this problem the next time the client recompiles. With C#, the problem could be a bit more difficult and labor intensive to track down (since there’s no easy way to detect this statically or even report on what exceptions a given API could possibly throw, a la JavaDocs). Both would likely result in nasty runtime bugs, however. I’d love to see a feature in Reflector (well, a VS MDA would be even better) which computes the possible exceptions a method invocation could leak. This is a bit tricky because a deep call graph traversal needs to occur, but I’d even take a list of exceptions thrown directly by the method in question.

Those perf architects are seldom wrong. For instance, when they recommend that you provide an explicit override implementation of the Equals(object) method for your value types, it'd be wise to listen. Unless you intend to never compare your instances for memberwise equivallence, that is.

In fact, not heeding this particular advice causes your value types to fall back to the System.ValueType implementation of Equals(). ValueType.Equals() takes an object parameter, causing value types to box as they're handed off to this method, and also uses reflection to determine memberwise equivallence. Needless to say, it's not overly performant for uses within loops, or other code with high performance requirements.

Specifically, the core of this implementation looks something like this (see here for the full Rotor implementation):

  public override bool Equals (Object obj) {

I'm in the process of reading the following books, all of which tickle me in a special way,

Algorithmics for Hard Problems: Introduction to Combinatorial Optimization, Randomization, Approximation, and Heuristics by Juraj Hromkovic Awesome read, covering various broad strategies to solving "hard" problems. Discusses deterministic, approximation, randomized, and heuristic approaches, at the same time providing realistic enough examples that the tradeoffs between each is made evident.

Eats, Shoots & Leaves: The Zero Tolerance Approach to Punctuation by Lynne Truss I'm still peeing myself. For punctuation nerds who are absolutely disgusted with the current state of English literary skills. This is a masterfully written, much appreciated break from my typical geekish read.

Free as in Freedom: Richard Stallman's Crusade for Free Software by Sam Williams I love historical accounts that spend entire chapters discussing PDP-10s and 11s. This book is all that and more, detailing the life one of the most eccentric and intelligent figures in the world of software. I've also read the following similar accounts, all of which I would highly recommend: The Cathedral and the Bazaar, Rebel Code, Just for Fun, The Art of UNIX Programming. Note: This book is available online for free... right here.

Game Physics by David H. Eberly This book is unfortunately primarily a refresher course in high school physics, perhaps university level, but there are a couple sections which make this one a keeper. I'd recommend it for reference, not something with which you'd want to curl up in front of the fireplace.

While I didn't read the following book cover to cover, I did read through about 50% of the material over the weekend.

Threat Modeling by Frank Swiderski, Window Snyder Written by a couple of my fellow Microsofties, this book details the threat modeling process in great detail. It's definitely a process book, and as such makes a few assumptions I would prefer to steer away from (e.g. lack of quantitative data showing why the investment in threat modeling is a Good Thing(tm)). That said, there is a lot of good material here.

So many books left to read, so little time.