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

[PVS-Help] extensible records: What is supposed to work?



Hi,

I did some first experiment with extensible records and got a "no
methods applicable" error (see
http://pvs.csl.sri.com/cgi-bin/pvs-bug?id=988). 

The release notes say that structural subtypes are work in
progress, especially wrt data types, which seem to be causing
above bug. Could somebody tell me if the above bug falls into the
"work in progress" part? When can I expect code like this to
work? 

When can I expect the following feature: Given a function

  f(a : record_type) : type_expr[record_type] = ...

that uses record update to compute the result and a record
extension of record_type to extended_record_type I want to apply
f to elements of extended_record_type. I can do that already with
the structural subtyping operator, as suggested in the release
nodes in the genpoints theory. However, I would like to do it
without the extra theory and the subtyping operator.

Bye,

Hendrik