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

K_conversion



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
 BEGIN
  K_conversion(x:T1)(y:T2): T1 = x
  CONVERSION K_conversion
 END K_conversion


With this feature the following theory typechecks.


K_conv : THEORY
BEGIN

  oops(f : [nat -> nat]) : nat
    = f(5)(10)

  damn(g : [nat -> [bool -> real]]) : real =
    g(5)(10)(TRUE)

END K_conv


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.

Best wishes,
Bart Jacobs.