Hello, and happy new year to everyone!
I'm pleased to announce that I will be holding a 90 minutes session at the next ACCU conference in Bristol. The abstract is given below.
The Bright Side of Exceptions
In many programming languages, the term "exception" really means "error". This is rather unfortunate because an exception is normally just something that does not happen very often; not necessarily something bad or wrong.
Some ancient languages like C don't support exceptions at all. You need to indicate them with specific return values from functions. Languages with explicit support for exceptions (e.g. Java, C++ or Python) provide built-in facilities for handling them. The most traditional approach to this is the "try/catch/throw" system, whatever it may actually be called in your favorite language. As it turns out, this system suffers from limitations which affect its usability in complex situations. The two major problems are 1. the obligatory stack unwinding on error recovery and 2. a two-levels only separation of concerns (throwing / handling).
In this talk, we will demonstrate the benefits of using a system which does not suffer from these limitations. More precisely:
- the stack is not necessarily unwound on error recovery, which means that the full execution context at the time the error was signaled is still available, - the separation of concerns is 3-fold: the code that signals an error (throw) is different from the code that handles the error (catch) which itself is different from the code that chooses how to handle the error (restart).
It turns out that an exception handling mechanism like this is able to handle more than just errors and in fact, even more than just exceptional events. In Lisp, this system is called the "condition" system. Conditions are the bright side of exceptions: not necessarily bad, not even necessarily exceptional. Conditions become an integral part of your programming paradigms toolkit. We will provide two examples of "condition-driven development". The first one will show how to handle actual errors, only in a more expressive and cleaner fashion than with a regular try/catch/throw system. The second example will demonstrate the implementation of something completely unrelated to error handling: a user-level coroutine facility.
We are please at the following paper has been accepted in the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Please find the title and abstract below.
Title and corresponding authors:
"Strength-based decomposition of the property Büchi automaton for faster model checking"' E. Renault(1), A. Duret-Lutz(1), F. Kordon(2), and D. Poitrenaud(2)
(1) LRDE-EPITA, www.lrde.epita.fr (2) UPMC-LIP6, www.lip6.fr
Abstract:
The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton.
When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm.
Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers.
-
Didier Verna -
Etienne Renault