After fixing this trivial bug, I'm able to move on to a slightly more complicated example. The source code is at
What the code trying to do is to put an element into an expansible container. Dafny will verify it if I turn on the assume statement at line 59.
I can definitely turn the assumption into a pre-condition of the Add() function. However, I would like to achieve the same effect at run-time. The reason is that I want to use this code as a C# library, asking the caller in C# to show that the argument is
not in the representation seems difficult.
The first few lines of the Add() function shows that the argument is not in the variable Contents, but what it takes to show that the argument is indeed not in the representation?