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:
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!
- Extended Static Checking for Java, Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe and Raymie Stata. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI), 2002. [PDF]
- The Spec# Programming System: An Overview, Mike Barnett, K. Rustan M. Leino and Wolfram Schulte, In Proceedings of the Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 2005. [PDF]
- Calysto: Scalable and Precise Extended Static Checking, Domagoj Babic and Alan J. Hu. In Proceedings of the International Conference on Software Engineering (ICSE), 2008. [PDF]
- Improving Computer Security using Extended Static Checking, B. V. Chess. In Proceedings of IEEE Symposium on Security and Privacy, 2002. [PDF]
- Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study, Frédéric Rioux and Patrice Chalin. Electronic Notes in Theoretical Computer Science, 157(2):119–132, 2006. [PDF]
- Faster and More Complete Extended Static Checking for the Java Modelling Language, Perry R. James, Patrice Chalin. In Journal of Automated Reasoning, 44(1-2):145–174, 2009 [PDF]
- Extended Static Checking for Haskell, Dana N. Xu. In Proceedings of the ACM workshop on Haskell, 2006. [PDF]
- Extended Static Checking: a Ten-Year Perspective, K Rustan Leino. Informatics, 2001. [PDF]
- An extended Static Checker for Modula-3, K. Rustan M. Leino and Greg Nelson. In Proceedings of the Conference on Compiler Construction, 1998. [PDF]
- Extended Static Checking, David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe. Compaq SRC Research Report 159, 1998. [PDF]