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

Re: [PVS-Help] Some problems in using PVS 3.2

Hi Nikhil,

This sounds strange to me.  Could you send me your specs, so I can try
them out and see if I can figure out what is going on?

Sam Owre

Nikhil Kikkeri <nikhil@engr.smu.edu> wrote:

> Hi--
> I do not know where to start but I'll try to be concise about the problem I am 
> facing. What I saying might be appear vague, but any solution at this point 
> would be helpful
> I have a big library of PVS files which were written in PVS 2.3 a couple of 
> years ago. For the purpose of our work we decided to migrate everything to 
> PVS 3.2.
> Just today I discovered some problems that might be associated with that. Or 
> it might be the case that it is a totally different issue.
> There are many circuits that are recursively described over the size of the 
> input "n" which is a posnat. These were proved using induct "n".  However I 
> found out that most of these proofs when re-run in PVS 3.2 generate more 
> sub-goals that what originally existed (for example 3 instead of 2).
> Ordinarily one could redo the proofs again manually and complete them. I tried 
> doing that but I faced a couple of other problems. For example 
> "bv2nat_concat" failed to replace the terms. For example in the consequent I 
> had
> bv2nat(fill[1](FALSE) o fill[1](x))
> If I say (use "bv2nat_concat") I get in the antecedent
> bv2nat[2](fill[1](FALSE) o fill[1](x)) = bv2nat[1](fill[1](FALSE))*exp2(1) + 
> bv2nat[1](fill[1](x))
> which is correct but the replace does not do anything. Also normally stating 
> (use "bv2nat_concat") does not produce the expressions with the parameters in 
> them. So this is the first time I have seen something like it.
> Doing C-u M-x show-expanded-sequent and then using that for the replace does 
> not seem to work either.
> Thank you in advance.
> Best regards
> -Nikhil
> -- 
> Depart not from the path which fate has assigned you.