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

Variant records in PVS

Dear PVS helper,

How does one go about defining variant records in PVS?  My specific problem
is that I want to build a type HEAP whose elements include
various objects such as CONS cells, VECTORS, STRINGS, NUMBERS, and so forth.

Can you point me to an example, say a binary cell space with atoms?