New subject: [proto] Implementing a type-and-effect system

26 Aug 2009

      I'm pondering the use of boost to implement a type-and-effect static 
checker which consists of:

1.  a system to define and name annotations
2.  a way to declare and associate class  members with the annotations
3.  a way to declare effects on methods that say how the method 
interacts with the annotation
4.  a way to capture uses of the members in the methods and verify that 
the effects are satisfied

A simple example might be logical heap partitioning and interference 
checking which in the *abstract* might look something like this:

class foo {
     heapregion a;
     heapregion b;

     foo * left in a;
     foo *right in b;

     foo *link();

     void update() reads a, writes b {
         right = a->link(); // ok
         left = /*anything*/ // fails, writing a
}

This is one very simple example, but hopefully illustrates the idea.

Ideally this can be all done statically at compile time without any 
run-time overhead, even if that means
a two-phase compilation process, a checking phase that instantiates the 
checking code, and an optimized compile phase that might not.
If this can be done via metaprogramming then we can avoid writing a new 
refactoring tool and/or modifying an existing front end.

I've been trying to determine whether to try and implement a custom 
system or use proto or is there something else that might help in this
effort?

Is anyone aware of similar uses of boost, other libraries, or have 
advice and/or feedback.

Thanks.

David

Implementing a type-and-effect system

david raila

Peter Schueller

david raila

tags

participants (2)