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

A question

Dear Sir,

I have a question:

We have a given record data type in PVS, like

Messages:type=[P:Char, Tm:Clock, Km:Index,No:nat]

How to present the "Tm"  through  the given "Message"?

is  Proj_2(Message) OK?
is there any other method?

Thank you very much!


Ren, Daqi
Electrical & Computer Engineering Department
Concordia University