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

Interpretations in PVS



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