Re: Light Formal Methods in GDB

[Michael Snyder <Michael.Snyder@palmsource.com>]

On Thu, 2006-10-12 at 15:07 +0100, Rob Quill wrote:
> Hi,
> 
> What I am aiming to do is allow the programmer to debug his program
> using linear temporal logic formulas to verify sections of code and
> check that specified properties hold.
> 
> I consider this important to be included in a debugger as it allows
> the programmer to stop the program execution at a certain point, and
> check at run-time that parts (or all) of the program are formally
> correct.
> 
> An example would be the Until operator, which allows the programmer to
> specify that expression A must be true until expression B is true.
> 
> I know this is a brief explanation, and if it unclear please feel free
> to ask me more about it, but I just wanted to see what people think of
> the idea.

Well, gdb can answer questions such as "is expression A true?", 
but only in the context of a specific, static point in the 
execution.  And gdb doesn't know anything about formal or temporal
logic.  Those are way outside its scope.

Are you thinking in terms of, say, a pre-processor that could
come up with a set of properties or propositions, translate them
into language that gdb can understand (eg. "stop here, and see if
expression A is true"), write the results to a file, and then
have a post-processor go over the results and test them against
the logical propositions?