[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: "MUNOZ, CESAR (LARC-D320)" <cesar.a.munoz@xxxxxxxx>*Subject*: Re: [PVS-Help] Induction on FSA*From*: Diego Martinoia <diego.martinoia@xxxxxxxxx>*Date*: Thu, 28 Feb 2013 19:44:25 -0500*Cc*: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>*Dkim-signature*: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:x-received:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=L2arZZVGWwGLY1DazwhjPvY/VdgpXr75/OJVuRutBIA=; b=cPuXPATBWWaWOcWChhl8quyrS1oYzkqCS1SP2Cwcf5JfgdKUld4GSrg93DqxtAO0dt wrmmELBRPWm9IQ0HbvqB+l5DnQ4r4Vnqhy+xbwPs9OHJ55lyDUQv6zrec3F4zDd+ohIK yN425pg4Vu4gF3Uufz5i+b+twb8tJimTO0+WORGat5OPqHGWaqkoV/RNMdxjO709lIJu waZdltGw0iyaxNm20Ahst3m9S7NvgCYMLw9RqQdkVpUp9wDLa6ztoHmkpmf/jEDsLDUo C8PW5g+UanaxmMJcmzCBgz7P08TVWypnXYUEdeMruvuC35SNp8S9apWTHbI2pGV/nRJQ HgZg==*In-reply-to*: <CD524A19.1945B%cesar.a.munoz@nasa.gov>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <CAF6EVK+7EkO-F6eOKatk+kuvJofkM-VWrxVG+5Ydw9RV8CwqEw@mail.gmail.com> <CD524A19.1945B%cesar.a.munoz@nasa.gov>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Dear Cesar, First of all, thanks for your reply. I had seen already that slides set as part of the Nasa virtual machine material. The project you linked me is very huge and I have quite some difficulties into following it (there are so many files that I hardly can find the beginning). The problem is that my theory is very convoluted, and recursive functions call other functions. I am now trying to prove them "step by step", by defining the inner behavior as lemmas to be proved from the inside out. But still, I get stuck even in the simplest cases. For example, I have a function defined as (t_Label_STAR_y is just a list of t_Label_y elements, which is a datatype that can be either addMatrix_y or removeMatrix_y, a disjoint union): alfa(org: t_Strings, newAuth: finite_set[t_TripleString]): RECURSIVE t_Label_STAR_y = IF empty?(newAuth) THEN null ELSE %Add the Auth cons(addMatrixCons_y(choose(newAuth)), %Add the Belongs W.Bel(sub,org) <--> Y.Mat(sub, org, sk(sub,org)) cons(addMatrixCons_y( (# e1:= choose(newAuth)`e1, e2 := org, e3 := skolem_generator_belongs(choose(newAuth)`e1, org) #) ), alfa_helper_joinCoalitionCons_w(org, rest(newAuth)))) ENDIF MEASURE card(newAuth) As you can see here, all I'm doing is appending addMatrix elements. This means that the list is either empty or composed only of addMatrix elements. So I have tried to prove the lemma: jc_help: LEMMA (FORALL (sy: t_States_y, lw: t_Labels_w): joinCoalition_w?(lw) IMPLIES (FORALL (ly: t_Labels_y): alfa(sy, lw)(ly) IMPLIES addMatrix_y?(ly)) ) And yet, if I use induct on lw I get stuck, after some trivial passages, as I don't have anything left quantified and I start "going down" in the recursion manually: {-1} list2set(cdr(cdr(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH)))) (ly!1) |------- [1] null?(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH)) {2} null?(cdr(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH))) [3] addMatrix_y?(ly!1) and on and on cdr(cdr(cdr( ... Suggestions? D. 2013/2/26 MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx>: > Diego, > > The technique depends on what you want to prove and how you defined your > recursive function. Please, take a look at this talk on recursion and > induction in PVS. > > > http://shemesh.larc.nasa.gov/PVSClass2012/pvsclass2012/lectures-printer/ind > uction.pdf > > A concrete example, which deals with a state automaton, can be found here: > > http://shemesh.larc.nasa.gov/people/cam/AirSTAR/ > > Hope that this helps, > > Cesar > -- > Cesar A. Munoz NASA Langley Research Center > Cesar.A.Munoz@xxxxxxxx Bldg. 1220 Room 115 MS. 130 > http://shemesh.larc.nasa.gov/people/cam Hampton, VA 23681-2199, USA > Office: +1 (757) 864 1446 Fax: +1 (757) 864 4234 > > > > > On 2/24/13 10:04 AM, "Diego Martinoia" <diego.martinoia@xxxxxxxxx> wrote: > >>Dear all, >> >>Greetings. >> >>I'm quite new to PVS, and I was wondering if anyone could help me: >> >>I am working on a theory that involves simulating finite state >>automaton, and I have to prove a lemma in the form: >> >>s1 = terminal ( s2, lx ) >> >>where s1 and s2 are states of the automaton, lx is a list of inputs >>(the labels on the automaton arches) and terminal is a recursive >>function defined as: >> >>terminal(s, lx) = >> >>IF null?(lx) THEN s >>ELSE >>terminal (next (s, car(lx)) , cdr(lx)) >> >>where next is the single step function of the automaton, car and cdr >>are the list accessors for the head and the rest of the list. >> >>Unfortunately, I can't figure out which commands allow me to deal with >>this kind of structure. I have tried launching a >> >>induct-and-simplify "lx" >> >>command, as well as similar form involving using the name and >>generalize-skolem-constants commands to have more possible argument >>for the induction rules, but I always fail. >> >>Anyone has any suggestions on the matter? >> >>Thanks, >> >>Diego Martinoia >> >

**Follow-Ups**:**Re: [PVS-Help] Induction on FSA***From:*MUNOZ, CESAR (LARC-D320)

**References**:**[PVS-Help] Induction on FSA***From:*Diego Martinoia

**Re: [PVS-Help] Induction on FSA***From:*MUNOZ, CESAR (LARC-D320)

- Prev by Date:
**Re: [PVS-Help] Induction on FSA** - Next by Date:
**Re: [PVS-Help] Induction on FSA** - Previous by thread:
**Re: [PVS-Help] Induction on FSA** - Next by thread:
**Re: [PVS-Help] Induction on FSA** - Index(es):