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

Re: [PVS-Help] A representation of symbols in PVS

Dear Aaron W. Hsu:

I think you can use "choose" function. These is an example which may be 
helpful for you.
----- Original Message ----- 
From: "Aaron W. Hsu" <arcfide@sacrideo.us>
To: "Natarajan Shankar" <shankar@csl.sri.com>
Cc: <pvs-help@csl.sri.com>
Sent: Tuesday, March 24, 2009 11:50 PM
Subject: Re: [PVS-Help] A representation of symbols in PVS

> Natarajan,
> Thank you for your message...
> On 24-Mar-2009 Natarajan Shankar wrote:
>> The simplest thing would be to define a datatype with a
>> single constructor "symbol" with an accessor name of type string
>> which is defined in the PVS prelude.  Another option is to leave
>> the symbol type as a type parameter that is instantiated as needed.
>> The choice depends on how you plan to use the data type.
> Hrm, on further evaluation, using the symbol type is useful, but now I
> have encountered another issue. I'd like for my expressions to contain
> any random elements of any type. That is, more than just symbols, I
> would like my s-expressions to contain numbers as well, for example. Is
> there a way of making a sort of generic type so that I can go through an
> s-expression and potentially obtain any sort of value?
> -- 
> Aaron W. Hsu <arcfide@sacrideo.us> | <http://www.sacrideo.us>
> "Government is the great fiction, through which everybody endeavors to
> live at the expense of everybody else." -- Frederic Bastiat
> +++++++++++++++ ((lambda (x) (x x)) (lambda (x) (x x))) ++++++++++++++

On the Verification of VDM Specification and Refinement withPVS.pdf