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

Re: [PVS-Help] Induction on FSA



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
>