From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 6444 invoked by alias); 12 Oct 2006 19:48:10 -0000 Received: (qmail 6435 invoked by uid 22791); 12 Oct 2006 19:48:10 -0000 X-Spam-Check-By: sourceware.org Received: from mx2.palmsource.com (HELO mx2.palmsource.com) (12.7.175.14) by sourceware.org (qpsmtpd/0.31) with ESMTP; Thu, 12 Oct 2006 19:47:58 +0000 Received: from localhost (localhost [127.0.0.1]) by localhost.domain.tld (Postfix) with ESMTP id 7AEFD26B24; Thu, 12 Oct 2006 12:47:57 -0700 (PDT) Received: from mx2.palmsource.com ([127.0.0.1]) by localhost (mx2.palmsource.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 08865-18-14; Thu, 12 Oct 2006 12:47:56 -0700 (PDT) Received: from ussunex01.palmsource.com (unknown [192.168.101.9]) by mx2.palmsource.com (Postfix) with ESMTP id 8909026AE0; Thu, 12 Oct 2006 12:47:56 -0700 (PDT) Received: from 192.168.92.75 ([192.168.92.75]) by ussunex01.palmsource.com ([192.168.101.9]) via Exchange Front-End Server owa.palmsource.com ([10.0.20.17]) with Microsoft Exchange Server HTTP-DAV ; Thu, 12 Oct 2006 19:47:57 +0000 Received: from svmsnyderlnx by owa.palmsource.com; 12 Oct 2006 12:47:55 -0700 Subject: Re: Light Formal Methods in GDB From: Michael Snyder To: Rob Quill Cc: gdb@sourceware.org In-Reply-To: References: Content-Type: text/plain Content-Transfer-Encoding: 7bit Date: Thu, 12 Oct 2006 19:48:00 -0000 Message-Id: <1160682474.14535.188.camel@localhost.localdomain> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 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/msg00081.txt.bz2 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?