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
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