This is the mail archive of the
gdb@sourceware.org
mailing list for the GDB project.
Light Formal Methods in GDB
- From: "Rob Quill" <rob dot quill at gmail dot com>
- To: gdb at sourceware dot org
- Date: Thu, 12 Oct 2006 15:07:02 +0100
- Subject: Light Formal Methods in GDB
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