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

Re: [PVS-Help] (no subject)



Hi,

PVS does not currently support this form of set.  There are two easy
options.  The first is to use the set expression with a predicate:

 s: set[t] = {x: t | x=a OR x=b OR x=c}

The other possibility is to use the list2set conversion that is defined in
the prelude:

 s: set[t] = (: a, b, c :)

Note that the conversion is automatically applied by the typechecker, as
if you wrote "list2set((: a, b, c :))".

The reason that the more direct form of set expression is not available is
because the set braces are used in the parser in a way that makes it
difficult avoid ambiguities, but I may work on fixing this at some point
in the future.

Regards,
Sam

> From:    "Feng Yuzhang" <fengyuzhang@hotmail.com>
> Subject: [PVS-Help] (no subject)
> Date:    Mon, 15 Dec 2003 08:55:55 +0000
> To:      pvs-help@csl.sri.com
> 
> Hi there,
> 
> I am a novice PVS user, so please forgive me if my question sounds silly.
> 
> My question is this:
> 
> Suppose I have a finite number of variables (say a, b and c) of type t and 
> would like to somewhat construct a set containing the variables.  Would it 
> be ok if I simply put
> 
> s: set[t]
> s = {a,b,c}
> 
> If not, what can I do?
> 
> The same question also applies to constructing a list.
> 
> Thanks!
> 
> _________________________________________________________________
> Find it on the web with MSN Search. http://search.msn.com.sg/