Light Formal Methods in GDB

[Rob Quill]

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.

Thanks,
Rob