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

Subject: Re: [Boost-users] [proto] Implementing a type-and-effect system
From: david raila (raila_at_[hidden])
Date: 2009-08-27 16:16:28

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