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

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

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.
Jerry James