From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 6428 invoked by alias); 13 Oct 2006 10:04:18 -0000 Received: (qmail 6416 invoked by uid 22791); 13 Oct 2006 10:04:17 -0000 X-Spam-Check-By: sourceware.org Received: from wx-out-0506.google.com (HELO wx-out-0506.google.com) (66.249.82.231) by sourceware.org (qpsmtpd/0.31) with ESMTP; Fri, 13 Oct 2006 10:04:14 +0000 Received: by wx-out-0506.google.com with SMTP id s19so839145wxc for ; Fri, 13 Oct 2006 03:04:12 -0700 (PDT) Received: by 10.70.76.11 with SMTP id y11mr4923430wxa; Fri, 13 Oct 2006 03:04:12 -0700 (PDT) Received: by 10.70.12.9 with HTTP; Fri, 13 Oct 2006 03:04:12 -0700 (PDT) Message-ID: Date: Fri, 13 Oct 2006 10:04:00 -0000 From: "Rob Quill" To: "Michael Snyder" Subject: Re: Light Formal Methods in GDB Cc: gdb@sourceware.org In-Reply-To: <1160682474.14535.188.camel@localhost.localdomain> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <1160682474.14535.188.camel@localhost.localdomain> 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/msg00087.txt.bz2 Hi, The principle works as follows: It it possible to create an automaton from an LTL formula, with expressions for values of variables as the transitions from one state to the next. Then the tricky part is building an automaton which represents the program. But once you have these it is possible to see if the automaton 'match' and if they do then the property holds. With regards to building the system automaton, at the very simplest you could single step the code, get values of variables at each step and make an appropriate transition on the automaton. However, this is obviously very inefficient, and improvements would most likely be made by building a control flow graph of the program (in some way) and use the nodes of that graph as the points get get values, or something like that. The advantage of including something like this in GDB is that once the property that the programmer expected to hold becomes false, program execution can stop and he programmer can use the standard GDB tools. Well, that'd be the idea anyway. The original idea was to do the same thing but for concurrent programs because there is research which says that using LTL formulas and the automaton technique, you can say whether properties of concurrent programs hold for all the possible interleavings. However, it was decided that that was too complicated, so it was narrowed to non-concurrent programs. Rob On 12/10/06, Michael Snyder wrote: > 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? > > >