What is Extended Static Checking?

Saturday, June 26th, 2010

Extended Static Checking (ESC) is the main technique used in Whiley. *But, what is it? *Since there isn’t a huge amount of information available on the web, I thought some discussion about this would be useful.

The term “static” implies that ESC is applied at Compile-Time — that is, when a program is constructed, rather than when it is run. The term “extended” implies it catches more errors than the convential techniques used in languages like Java. Extended Static Checking represents one point on a scale which ranges between making no effort to catch errors, up to performing (usually by hand) a detailed and rigorous proof that a program is correct. Roughly speaking, this scale looks something like this:

Here, I consider Languages like C and C++ to have no checking as, whilst they do have types, they are not strongly enforced and can cause arbitrary crashing at runtime (e.g. the infamous blue screen of death, or the equally annoying seg fault). Dynamic type checking includes languages like Python, PHP, JavaScript, Ruby, Lisp and SmallTalk (to name just a few). Here, the type system is strongly enforced at runtime to prevent arbitrary crashing, although type errors can still occur during execution. Extended dynamic checking is less common and represents efforts to check more detailed constraints at runtime. Examples of this include Eiffel, JML RAC, Contract4J and JContractor.

With dynamic checking, errors are not spotted until they actually occur during a program’s execution. Obviously, if this happens after the program has been released it is, at best, embarrassing and, in the worst-case, leads to catastrophic failure. Proponents of dynamic checking argue that modern software development processes, with their strong emphasis on software testing, dramatically reduce the chances of this happening. In many situations, the risk is out-weighed by the ease of development offered by dynamically checked languages. However, in situations which are saftey-critical or where very large and complex systems are being developed, more rigorous techniques are necessary.

This is where static checking comes into play. The advantage of static checking over dynamic or runtime checking is that it happens before the program is ever run. Thus, we have a guarantee that certain kinds of error can never happen during a program’s execution. Obviously, this is desirable, but it comes at a cost. Programming in statically checked languages is often more involved and requires strict adherence to certain rules. Static type checking covers the majority of statically checked programming languages, including Java, C# and Haskell. In this case, each program variable is given a fixed type (e.g. string, int, real, etc) and the language guarantees it only ever holds values of this type. However, whilst this is certainly useful, it accounts for only a small fraction of the errors which can arise during a program’s execution.

Extended Static Checking attempts to take this further by catching a much larger range of errors. The aim is to be fully automatic — meaning no human intervention is required. Examples of errors which can be caught using this technique include division-by-zero, array out-of-bounds, integer overflow and null dereferencing. The technique enforces detailed constraints on what values a program variable may hold. For example, that an integer variable can only hold values between 1 and 7 (since it represents a day of the week). Modern languages like Java cannot statically check constraints such as this and, hence, variables may hold incorrect values during execution. The term “Extended Static Checking” is really a catch-all for a range of techniques developed and used in both academia and industry over the last 40 years, including static analysis, abstract interpretation, model checking, SAT solving and automated theorem proving. Languages which employ extended static checking are few and far between, and none has yet made it into the mainstream. Examples include Spec#, JML (via ESC/Java), Dafny, SPARKada and, of course, Whiley.

Going beyond extended static checking moves us into the area of full formal verification. Here, pretty much anything goes in an effort to prove that a program is correct with respect to a specification or property of interest. Proofs are often done by hand, although mechanical proof assistants, such as HOL, Isabelle and Coq, are increasingly used to help manage the complexity. A proof assistant is a tool for developing proofs which can help automate much of the grunt-work involved, but which still relies on a human operator to make important decisions. A good example of a recent full verification project is that of the Microsoft Hypervisor, where VCC was used in proving 50,000 lines of C code were correct.

Anyway, I think that’s enough for now!

What is Extended Static Checking?

Further Reading