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

[PVS-Help] Override expressions

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]
 indices: TYPE = setof[index]
 change(a: arr, iset: indices): arr = a := WITH [ (i) = 20 ]

'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.