Articles

What is Extended Static Checking?

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:

Range of Checking Techniques used in Programming Languages

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!

Further Reading

  • 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 LeinoInformatics, 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]

See also the talk on Extended Static Checking by Greg Nelson over on ResearchChannel, and also the discussion of Strong Typing over on C2.  The ESC/Java tool is also available for download from here.

http://research.microsoft.com/en-us/projects/specSharp//

6 comments to What is Extended Static Checking?

  • If the spec says function A returns 3 and function B takes an integer in the range 1 to 10 inclusive, and returns its argument multiplied by the value from calling function A.

    Will the Whiley type system catch the error of actually providing a function A that returns 2?

    What if function A returns the string “3″?

    Or if function A uses up too much of a runtime resource before returning 3?

    What if the spec should have read that function A should return 10?

    How far along does Whiley get you when your customer is often vague about their requirements? Avoiding a BSOD is only one aspect of fulfilling a customers needs.

    Are such extended type checks best done as a post process? After all, how much will it help in agreeing a spec, or getting a customer basic services now rather than promised fluff later?

  • If the system runs out of resources, or your customer was too vague … it’s not going to help.

    You won’t be able to return a string when a function is declared to return an int (as in Java).

    Not following you on the first bit though.

    Basically, the point is that if you know what want, it’ll help you make sure you’ve got it. That’s at least one aspect of the problem that will be simplified…

  • Note that “correct” in the context of verification means “Contains all errors of the specification”. While this appears nitpicky, but I consider this to be important enough to mention it often.

    Also, I would like some sort of key to the scale. I think what you want to convey with the scale is: On the top of the scale, the probability of certain classes of errors is high, while the probability of these classes of errors is small on the bottom of the scale. (At first, I wanted to reject this figure, but then I kept pondering how it was meant, and I think this fits)

  • Hi Dave, thanks for the reply. You mentioned in your summary “the point is that if you know what you want …”. Unfortunately I get the impression that customers need to work with the programmers to develop a good spec. In that case, being able to get a quick initial prototype out can be invaluable in helping to hone the spec and drive successive iterations of the deliverable.

    In these cases a programmer shouldn’t spend too much time on boilerplate so things like a clear, concise syntax, good type inferencing, fast builds and easy testing might pay big dividends.

    I wish you well with the Whiley language.

  • Hi Paddy,

    So, basically I agree with you. Whiley is most likely more suited to e.g. safety-critical applications where it’s extremely important to have a low error count.

  • Hi Tetha,

    I think your analysis based on probability is a good one. And, generally, following on from what Paddy is saying, how much the risk bothers you will determine what approach is best.

Leave a Reply

 

 

 

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>