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

*To*: Diego Martinoia <diego.martinoia@xxxxxxxxx>*Subject*: Re: [PVS-Help] Induction on FSA*From*: "MUNOZ, CESAR (LARC-D320)" <cesar.a.munoz@xxxxxxxx>*Date*: Fri, 1 Mar 2013 08:58:56 -0600*Accept-language*: en-US*Acceptlanguage*: en-US*Cc*: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>*In-reply-to*: <CAF6EVKLRHaoxhkE2Cp8P6_3bUVqMYrtfPn5vzT4nKoSMYg6kZA@mail.gmail.com>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*Thread-index*: Ac4WjU0zPBEB9RoHQsKTh1qqL1M06g==*Thread-topic*: [PVS-Help] Induction on FSA*User-agent*: Microsoft-MacOutlook/14.2.3.120616

Diego, I have a few comments regarding your specification. First, since "lw" is a finite_set you cannot directly apply (induct "lw"). I suspect that you have used the induction schema "finite_induction" provided in the prelude. However, that's not the easiest way to proceed. My second comment is that when you write alfa(sy,lw)(ly), PVS implicitly adds a conversion from lists to sets, since the membership predicate l(x), where l is a list and x is an element, is not directly supported by lists. This adds unnecessary complications to what you are trying to prove. You can use instead FORALL(k:below(length(l)): Š nth(l,k) Š to refer to a particular element of the list. Or, even better, the predefined predicates "every" and "some" already defined for lists. Finally, as it is explained in the slides, PVS provides a simple way to prove inductive properties without the use of explicit induction (look for the section on "induction-free induction"). I have simplified your problem to this one: diego : THEORY BEGIN s : VAR finite_set[nat] evens(s) : RECURSIVE { l: list[nat] | every(even?,l) } = IF empty?(s) THEN null ELSE cons(2*card(s),cons(2*choose(s),evens(sets.rest(s)))) ENDIF MEASURE card(s) n : VAR nat evens_is_sound : LEMMA every(even?,evens(s)) END diego Notice the return type of evens. Because of this type, the proof of the lemma is just (subtype-tcc). There is no free lunch, but almost. PVS generates 4 TCCs, all of which are easily proven. I attach the pvs and prf files to this message. 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/28/13 7:44 PM, "Diego Martinoia" <diego.martinoia@xxxxxxxxx> wrote: >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/i >>nd >> 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 >>> >>

**Attachment:
diego.pvs**

**Attachment:
diego.prf**

**Follow-Ups**:**Re: [PVS-Help] Induction on FSA***From:*Diego Martinoia

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

- 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):