Overlapping Lvals

[DavePearce]

Does this make sense:

method main(int[] xs, int i, int j):
    xs[i],xs[j]= 0,1

What is the semantics of this? Dafny disallows this.

[utting]

If you want to allow overlapping lvals, I think it should generate a proof obligation:

assert i != j;

or perhaps more generally:

assert i == j ==> rhs1 == rhs2 (0 == 1) in this case.

[DavePearce]

Hey,

Yeah, so that second obligation is interesting. I'll have to have a think, but yeah definitely one of these two makes sense.