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

Re: [PVS-Help] arrays




Sujith: You could do the initialization with a long if-then-else
chain, but the easiest approach is to use the list2finseq conversion
from the prelude.  This way you can give the array as as a list
that is then converted to a finite sequence.

-Shankar

sujith cs <cs_sujith@hotmail.com> wrote:

> sir, i am doing my pg project using PVS. i have to use array concept in this
> specification
> for eg.
>   int array[10]={1,3,2,4,5,7,5,9,1,0};
> in PVS i defined array as follows.
> arr: TYPE=  [conf_unsigned16 ,[conf_short_int->elem]]
>  i have to give initial values to this array.
> i gave values as follows.
> (10,(lambda i: if i=0 then 1 elsif i=1 then 3 elsif i=2 then 2 elsif i=3 then 4
> ............ else 0)). 
> i want to know whether it is correct or not.
> is there any other methods for giving initial values. please help.
> sujith
> 
> -------------------------------------------------------------------------------
> http://windows.microsoft.com/shop Find the right PC for you.