Re: Interpretations in PVS

[Sam Owre <owre@csl.sri.com>]

Hi Maria José,

The current implementation of theory interpretations won't allow
you to map finite_sets to lists, as finite_sets is interpreted.
In the future we hope to allow such mappings.

Of course, you could create an abstract Finite_Sets theory, where
the type is uninterpreted, define the basic set operators and
build in all the finite set (and set) axioms.  You could then
show that the current finite_sets is one refinement, and
(equivalence classes of) lists is another.

Another approach would be to define a function that converts
finite sets to lists, and declare it to be a conversion.  Then
define your computable functions over lists, and when they are
given finite set arguments the conversion will be applied
automatically.

PVS 3.0 is a beta release right now - we're working hard to
produce the next release.  It will be announced on the PVS
mailing list when it's ready.

Regards,
Sam Owre

> From:    Maria-Jose.Hidalgo@cs.us.es
> Subject: Interpretations in PVS
> Date:    Wed, 02 Oct 2002 11:31:01 +0200
> To:      shankar@csl.sri.com
> CC:      pvs-help@csl.sri.com
> 
> Hello,
> 
>  I'm working wiht PVS 2.4 and I use the type of finite sets to specify
> the objects in a theory T. I'm interested in making another theory T'
> which is a refinament of T, such that in T' it could be calculated the
> functions. So, I want to interpret
> finite sets by lists, in a general form.
> 
> I have just read the paper "Theory Interpretations in PVS" and I found
> it really intersting. This paper shows how we can interpret a type
> noninvariant or a datatype by another one, but I don't see how could a
> type like finite sets be interpreted. It is posible in PVS 3.0?
> 
> Thank you for your help...
> 
> María José Hidalgo
> 
> Dpto. Ciencias de la Computación e Inteligencia Artificial
> Universidad de Sevilla
> Spain