When there are two or more array input parameters in a method

[dreamqin68]

Hi all,

I'm a new user of Dafny. I have a question and hope to get help. Thanks.

When a method has two or more array input parameters, the other array may also be changed if one of the arrays is modified.

method test(a:array<int>, b:array<int>, element:int)
    requires a.Length > 0 && b.Length > 0
    modifies b
{
   b[0] := element;
   assert a[..] == old(a[..]);
}

The assertion above might not hold. The counter-example given shows that the two arrays may be equal.
Then I take requires a!=b as a precondition. The assertion now holds.

(1) When a method has two or more array inputs, do I need to add this precondition(requires a!=b) every time? Or is it correct to add this precondition so that the assumption holds?

(2) I didn't write a in the modifies clause, but a still may be changed. Why?

[MikaelMayer]

Hello @dreamqin68 ,
This is a very nice demonstration of how Dafny can prevent aliasing errors, thanks !
(1) What you did is correct, you either have to add a != b as a precondition, or wrap the assignment in a if a != b { ... } construct.
(2) I tried to replace b[0] := element; by a[0] := element; but it correctly indicates assignment might update an array element not in the enclosing context's modifies clause. Can you please detail your example?

[dreamqin68]

Thanks for your reply!

(2)What I mean is that even in the case where the two arrays are the same a==b, when there is only b in the modifies clause, it should only change b. I think since both arrays are input parameters, we can choose to change only one of them.

[MikaelMayer]

When you write a[0], it will try to prove that a in X is true, if modifies X is the modifies clause surrounding it. Since à == b and X = {b}, it can prove that a in X even though it's modifies {b}.

That's beautiful although I understand it might not serve your use case that you describe. However, why name things two different ways if we know they are equal? That'd be a source of bugs, no? You can always pretend you read only from one and write only in another, but you'd be writing in the same anyway.

[dreamqin68]

Yeah, thank you!