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

Subject: Re: [Boost-users] Implementing a type-and-effect system
From: Peter Schueller (ps_at_[hidden])
Date: 2009-08-27 02:48:10

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<raila_at_[hidden]> 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_at_[hidden]
> http://lists.boost.org/mailman/listinfo.cgi/boost-users
>
>