Pondering Pre/Post Conditions to Enforce Software Correctness

That other software company has a some brilliant people working on verifying their source code. Their approach is hardcore and seems quite good. Their recipe to robust C# (applying this to C is research-in-progress, C++ isn’t yet considered) code is:

  • sprinkle pre/post-conditions for functions. Reduce annotation labour by additional rule inference
  • dataflow analysis to verify type-system stuff like not-null annotations
  • Abstract interpretation + model checker to enforce pre/post-conditions
  • BoogiePL intermediate language. Anything can be accomplished by an awesomely named intermediate language!

Resulting code runs fast has a lot fewer bugs than code without all this fancy machinery. Unfortunately, the benefits can only be reaped if a whole program gets annotated. Otherwise, the model checker gets frustrated. Essentially the language being checked is turned into another much safer (more boogie!) language. I’m looking forward to the day (that will never come) when all new C code is written this way.

If adding these to source code makes you rewrite the whole program, wouldn’t it be easier to invent another low-level language that comes with safety by default?

I am guessing that the dehydra method of checking for a relatively small number of application specific bugs is the most practical approach available and it will get us 60% towards Boogieing. Now that elsa has support for preprocessor macros it should be possible to specify non-formal pre/post-conditions to check for common errors. It’s merely a complicated question of defining what should be checked for.

I don’t have the motivation to write/buy/adopt/integrate a formal tool like a model checker, but it seems that it’s possible to write application specific checks in JavaScript that can run circles around what most model checkers can do.

That other company isn’t the only vendor working on this stuff. There brilliant people taking a somewhat different (and open source) approach.

3 comments

  1. Hm, like a design-by-contract library for JavaScript? Or xpcshell tests? Or perhaps the D language?

  2. I guess I forgot to mention the key point of this. The BoogiePL contracts are enforced at compile time so your program is rejected if it doesn’t comply. However Spec# also complements these with runtime checks when only part of the code is annotated.

    I suppose something similar would be possible with es4

  3. ES4 does have extensible type annotations for args and return values, and it will enforce them at runtime if it can’t prove they’re violated with its optional static checker. But no rule inference, no data flow analysis, etc. Non-nullable types must be initialized early enough, for class instance vars with special constructor syntax.

    See http://ecmascript-lang.org/ for the reference implementation, which supports a lot (but not all, and not all bug-free) of what will be in ES4.

    /be