Question about the dynamic frame idiom

Oct 21, 2012 at 10:09 PM


Following the suggestion at (thanks, Rustan!), I'm trying to learn the idiom of dynamic frames.

I wrote a single linked list program (please see, but Dafny seems unable to connect the dots.

I'm confused that why Dafny will unable to prove the assertion.

Thanks for your help.

class A {
  function Valid() : bool
    reads this, Repr;
    this in Repr && null !in Repr

class AHolder {
  method Add(val : A)
    requires val != null && val.Valid();
    // assertion violation
    assert val.Valid() ==> null !in val.Repr;

Oct 21, 2012 at 10:33 PM

The problem has nothing to do with dynamic frames.  But in the definition of Valid(), you have written

A && B && C ==> (D && E && F && G)

when you mean

A && B && (C ==> D && E && F && G)

Note that && binds stronger than ==> (as may be suggested by the respective widths of the operators, meaning the number of ASCII characters it takes to write them).

With that change, your program verifies:


Oct 22, 2012 at 4:26 AM

Thanks! I really need to learn more about Dafny and operator precedence...

Oct 23, 2012 at 4:38 AM

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?