Quantifying over map.Keys has quadratic runtime in Java

[robin-aws]

Dafny version

4.1.0

Code to produce this issue

method Main() {
  var s := seq(100_000, x => x);
  var m := map k <- s :: k := k;
  var m2 := map k <- m.Keys :: k + 10 := k;
}

Command to run and resulting output

% dafny run -t:java src/Scratch.dfy

What happened?

Command takes about 2 minutes to complete. Replacing m.Keys with m makes it take 10 seconds.

Root cause appears to be translating m.Keys to DafnyMap.keySet(), which makes a defensive copy of the underlying map's key set.

What type of operating system are you experiencing the problem on?

Mac

[atomb]

I wouldn't consider this a soundness issue. It's perhaps a serious issue, but the program does still compute the correct result. I can remove the label unless anyone objects (@keyboardDrummer?).

[keyboardDrummer]

I wouldn't consider this a soundness issue. It's perhaps a serious issue, but the program does still compute the correct result. I can remove the label unless anyone objects (@keyboardDrummer?).

I think an incorrect computational complexity can cause a program that should terminate, to seemingly not terminate at all, which I would consider a failure to compute the correct result.

But I'm happy to agree to disagree, feel free to remove the label.

[atomb]

I wouldn't consider this a soundness issue. It's perhaps a serious issue, but the program does still compute the correct result. I can remove the label unless anyone objects (@keyboardDrummer?).

I think an incorrect computational complexity can cause a program that should terminate, to seemingly not terminate at all, which I would consider a failure to compute the correct result.

Yeah, I understand that reasoning. It's not part of what's usually considered to fall in the category of soundness, though, so I think it might wind up being more confusing than helpful in the long run.

But I'm happy to agree to disagree, feel free to remove the label.

Okay, I'll do that.