From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 3493 invoked by alias); 12 Oct 2006 14:07:10 -0000 Received: (qmail 3333 invoked by uid 22791); 12 Oct 2006 14:07:09 -0000 X-Spam-Check-By: sourceware.org Received: from wx-out-0506.google.com (HELO wx-out-0506.google.com) (66.249.82.237) by sourceware.org (qpsmtpd/0.31) with ESMTP; Thu, 12 Oct 2006 14:07:05 +0000 Received: by wx-out-0506.google.com with SMTP id s19so567527wxc for ; Thu, 12 Oct 2006 07:07:03 -0700 (PDT) Received: by 10.70.32.13 with SMTP id f13mr3020561wxf; Thu, 12 Oct 2006 07:07:03 -0700 (PDT) Received: by 10.70.12.9 with HTTP; Thu, 12 Oct 2006 07:07:02 -0700 (PDT) Message-ID: Date: Thu, 12 Oct 2006 14:07:00 -0000 From: "Rob Quill" To: gdb@sourceware.org Subject: Light Formal Methods in GDB MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline X-IsSubscribed: yes Mailing-List: contact gdb-help@sourceware.org; run by ezmlm Precedence: bulk List-Subscribe: List-Archive: List-Post: List-Help: , Sender: gdb-owner@sourceware.org X-SW-Source: 2006-10/txt/msg00078.txt.bz2 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