This is the mail archive of the
gdb@sourceware.org
mailing list for the GDB project.
Re: Light Formal Methods in GDB
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?