1

The question is rather simple: why does the assertion bellow return "assertion violation".

method test()
{
  var a := new int[5];
  a[0] := 1;
  a[1] := 1;
  a[2] := 2;
  a[3] := 3;
  a[4] := 3;
  var b := new int[3];
  b[0] := 1;
  b[1] := 2;
  b[2] := 3;
  assert(forall i :: exists j :: ((0 <= i < 5) && (0 <= j < 3)) ==> (a[i] == b[j]));
}
user2009400
  • 147
  • 9

1 Answers1

2

Here's one way to fix it. Add the following assertions before your assertion.

assert b[0] == 1;
assert b[1] == 2;

It seems that under a quantifier can only remember the value of the most recent assignment to b, which explains why no extra assertion about b[2] is required.

James Wilcox
  • 5,307
  • 16
  • 25
  • 2
    I find it really hard to use Dafny due to this type of situation. I feel like I'm permanently missing out on some of the rules by which the language operates... – user2009400 Apr 10 '18 at 15:24