Re: [Boost-users] [proto] Implementing a type-and-effect system

I thought that proto might be my path to enlightenment rather than building or modding a front-end On 08/27/2009 01:48 AM, Peter Schueller wrote:

I think you are looking for a model checker, which verifies if some condition is true for all possible executions of some part of code.

This is a very non-trivial task in general. I'm not sure if such a tool is usable for C++ at the moment, but there are several scientific projects for C:

BLAST http://www.cs.ucla.edu/~rupak/blast/

MAGIC http://www.cs.cmu.edu/~chaki/magic/

The Windows Driver Development Kit also uses a similar technique to check if the driver correctly uses the Windows API: Their project is called SLAM http://research.microsoft.com/en-us/projects/slam/

Best, Peter

On Wed, Aug 26, 2009 at 20:32, david raila wrote:

...

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 _______________________________________________ Boost-users mailing list Boost-users@lists.boost.org http://lists.boost.org/mailman/listinfo.cgi/boost-users

_______________________________________________ Boost-users mailing list Boost-users@lists.boost.org http://lists.boost.org/mailman/listinfo.cgi/boost-users