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

Variant records in PVS

Steve Johnson writes:
 > 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.


You use the abstact datatype mechanism for this.

Here is an example of IEEE 854 floating point numbers:

  fp_num: datatype
    infinite(i_sign:sign_rep): infinite?
    NaN(status:NaN_type, data:NaN_data): NaN?
   end fp_num

-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/