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

Re: [PVS-Help] Induction on FSA


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. 


A concrete example, which deals with a state automaton, can be found here:


Hope that this helps,

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,
>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
>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?
>Diego Martinoia