www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - LLVM talks 2: TESLA

Second interesting thing I've found from the 2011 LLVM Developer Meeting:

In the "Integrating LLVM into FreeBSD" talk I have seen a reference to TESLA
(the talk itself is not interesting). It's not so easy to find good info about
TESLA, I have found this little tutorial:

And two examples:

From the page:

What is the TESLA?
TESLA is a framework for testing temporal properties of a software written in
the C language. Standard assertions i.e. assert(3) are able to test simple
expressions which refer only to an actual state of a program, testing temporal
properties in this case (e.g. conformance with the protocols, condition checks
before usage etc.) is complex, requires additional code and data structures,
thus it could be a source of unnecessary complexity and bugs. TESLA introduces
assertions which test temporal expressions, it means that it's able to refer to
the future and to the past, which is a great help when a goal is to verify some
property which refers to the time, i.e. check if access control checks were

You write a simple automata like this using temporal logic:

automaton simple_protocol() {
  void main(struct test *t) {
    t->state = P1;
    multiple {
      either {
        t->state = P2;
      } or {
        t->state = P3;
    either {
      t->state = P4;
    } or {
      t->state = P5;
    t->state = P6;

And the TESLA tool adds asserts (and small functions that contain asserts) to
your C code that enforce those temporal constraints.

It seems nice, its purpose seems similar to the typestates of the Rust
language, but this works on C programs.

Dec 16 2011