[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Interpretations in PVS
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
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.
> From: Maria-Jose.Hidalgo@cs.us.es
> Subject: Interpretations in PVS
> Date: Wed, 02 Oct 2002 11:31:01 +0200
> To: email@example.com
> CC: firstname.lastname@example.org
> 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