[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Interpretations in PVS
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