[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Some problems in using PVS 3.2
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
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.
Depart not from the path which fate has assigned you.