[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.

Steve,

You use the abstact datatype mechanism for this.

Here is an example of IEEE 854 floating point numbers:

  fp_num: datatype
   begin
    finite(sign:sign_rep,Exp:Exponent,d:digits):finite?
    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/