[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