[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Override expressions
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.