Re: [PVS-Help] Override expressions

["Jerry James" <loganjerry@xxxxxxxxx>]

On Sat, Mar 15, 2008 at 10:14 AM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> I'm having trouble getting my override expression to
>  typecheck. Essentially, I have an array and would like to alter a
>  subset of the values. For example:
>
>   [1, 2, 3] (change values 1 and 2) becomes [20, 20, 3]
>
>  What I have now is
>
>   arr: TYPE = [nat->nat]

With this definition, all of your arrays are infinite.  Is that what you want?

>   indices: TYPE = setof[index]

What is the definition of type 'index'?

>   change(a: arr, iset: indices): arr = a := WITH [ (i) = 20 ]

Is the intent that the value stored at each index in 'iset' is made to
be 20?  If so, perhaps you want something like this.  WARNING: this is
untested.  I am unfortunately sitting at a Windows machine with no PVS
installation in sight.

change(a: arr, iset: indices): arr = LAMBDA (i: nat): IF member(i,
iset) THEN 20 ELSE a(i) ENDIF

>  'i' should be an individual index within the 'iset', but of course
>  here it doesn't have a "resolution". On the other hand, the following
>  will typecheck:
>
>   change(a: arr, iset: indices): arr = LAMBDA(i: (iset)): 20
>
>  but I'm not sure that it's returning what I want. Any insight is
>  appreciated. Thanks in advance.

That definition gives you an array in which every index in iset maps
to 20, but it doesn't say what indexes not in iset map to.  If I had
to guess, I would guess that PVS adds an 'extend' to the right-hand
side making those indexes map to zero.
-- 
Jerry James
http://loganjerry.googlepages.com/