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

Re: K_conversion

Bart,

The next patch will allow some control over conversions,
and I will make sure that K_conversions are not used by
default.

For now, the simplest way to find out what conversions
are being used is to use M-x show-pvs-file-messages (or
show-theory-messages), as this shows all the conversions
that were used.

Sorry for the inconvenience this caused.

Sam Owre

> From:    Bart Jacobs <Bart.Jacobs@cs.kun.nl>
> Subject: K_conversion
> Date:    Thu, 25 May 2000 15:25:05 +0200
> To:      pvs@csl.sri.com
> cc:      Bart.Jacobs@cs.kun.nl
> 
> 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.
Follow-Ups: References: