CODEWITHSUNDEEP
dafny
jiplucap
jiplucap

Reputation: 164

Dafny unexpected assertion violation

Why Dafny is not able to prove this?

method Main() {

assert forall f:map<string,int>, x:string, v:int :: x in f.Keys  ==>  f.Values- 
{f[x]} + {v} == (f[x:=v]).Values;

}

Upvotes: 1

Views: 480

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

The assertion is not true if f contains duplicate values. For example, consider the map 

var f := map[1 := 0, 2 := 0];

which satisfies

assert f.Values == {0};

Now make an updated map by setting the key 1 to have value 7, 

var f' := f[1 := 7];

Then f'[1] == 7 and f'[2] == 0, so f' satisfies

assert f'.Values == {0, 7};

but your assertion would imply f'.Values == {0}, which is false.

For the second question you asked in a comment, the assertion is true, but Dafny cannot prove it because of a triggering problem. You can convince Dafny to prove it by saying

var f' := f[x:=v];          // give updated map a name for convenience
assert f'[x] in f'.Values;  // triggers axiom about .Values
assert v in f'.Values;      // now this verifies

For more information about triggers, see the FAQ. You may also be interested to read the axiomatic definition for the .Values primitive operation.

Upvotes: 1

Related Questions