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

Re: [PVS-Help] how to use "list" which is in pvs prelude

In PVS, you could also write lists using the following notation:

(: 1, 2, 3 :).


Jerry James wrote:
> 2008/5/10 applehopedream <applehopedream@xxxxxxx>:
>>   I want to use a list with a certain length and certain elements ,but I
>> don't know how to set the length and elements.
> If you mean the list datatype defined in the PVS prelude, then "null"
> is the empty list and the "cons" operator adds elements onto the front
> of a list.  So if I want a list of length 3 containing the natural
> numbers 1, 2, and 3, in that order, then I would write:
> cons(1, cons(2, cons(3, null)))
> The list2finseq theory in the prelude also has a function that
> converts finite sequences into lists.  For more information on
> datatypes, see http://pvs.csl.sri.com/documentation.shtml.

Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4