[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Dear PVS users,
I would like to bring up the issue of K_conversion's on this list.
They are introduced in the prelude as:
K_conversion [T1, T2: TYPE]: THEORY
K_conversion(x:T1)(y:T2): T1 = x
With this feature the following theory typechecks.
K_conv : THEORY
oops(f : [nat -> nat]) : nat
damn(g : [nat -> [bool -> real]]) : real =
This means that mistakes that are easily made are not
detected by the PVS typechecker.
I must say that I find this *very* annoying. I have lost
many hours because of such K_conversions, for example
because they became clear only after a detailed analysis
of why a certain proof does not work.
I know that one can see if K_conversions are inserted by
checking the messages after typechecking. But this requires
an extra effort. The most important problem I have with
this feature is that the typechecker does not tell me anymore
whether my PVS file is type correct.
This is a particular nuissance because at Nijmegen we do a
lot of automatic PVS code generation. With K_conversions we
still don't know after typechecking if the generated code
is correct. Also, we do lots of proofs by automatic rewriting.
If these proofs fail, it takes much time to find out why.
Therefore, I am interested to know if other PVS users share
my (negative) experiences with K_conversions.
And also whether the developers are willing to remove this
feature (or at least to make it a non-default option) in a
next version of PVS.