[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Some problems in using PVS 3.2
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?
Nikhil Kikkeri <firstname.lastname@example.org> wrote:
> 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
> bv2nat(fill(FALSE) o fill(x))
> If I say (use "bv2nat_concat") I get in the antecedent
> bv2nat(fill(FALSE) o fill(x)) = bv2nat(fill(FALSE))*exp2(1) +
> 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
> Depart not from the path which fate has assigned you.