search

Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
219 stars 36 forks source link

Overlapping Lvals #1057

Open DavePearce opened 3 years ago

DavePearce commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

Hey,

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