"reads" and "termination" errors

Mar 17, 2016 at 6:46 PM

I have some "reads" and "termination" errors for the following code (http://rise4fun.com/Dafny/zHqA):

class Tree{ 
    var left : Tree;
    var right : Tree;
    var val : int;

    ghost var repr: set <object>;

  function Valid(): bool
    reads this, repr;
    this in repr &&
    ((left == null && right == null) ||
    (((left != null) ==> (left.repr < repr && this !in left.repr && left.Valid())) &&
    ((right != null) ==> (right.repr < repr && this !in right.repr && right.Valid()))
i.e. on line
    (((left != null) ==> (left.repr < repr && this !in left.repr && left.Valid())) &&
    ((right != null) ==> (right.repr < repr && this !in right.repr && right.Valid()))
However, if I add "left in repr" and "right in repr", these errors go away. These two are, in my mind, logically redundant, as "left in repr" can be inferred by "left.repr < repr" and "left in left.repr".

What did I miss here ?

Thanks in advance.

Mar 19, 2016 at 12:30 AM
Yes, from left in left.repr and left.repr < repr, it follows that left in repr. However, where does left in left.repr come from? It can only come from left.Valid() and the definition of Valid. But to prove that the call to left.Valid() terminates, you must prove the decreases clause of the call left.Valid() (which is left.repr + {left} -- since no explicit decreases clause is provided, Dafny constructs this one from the reads clause) to be a strict subset of the decreases clause of Valid() (which is repr + {this} -- hint: if you're unsure of what these automatically constructed decreases clauses are, inspect the hover text in the Visual Studio or emacs IDE). That, in turn, is true only if left in left.repr! So, there is a circularity you need to break.

The standard way to break this circularity is to write the line above as:
left != null ==> left in repr && left.repr <= repr && this !in left.repr && left.Valid()
I would recommend doing this. (That's also what you get if you make use of the {:autocontracts} attribute.)

Note, there's one other difference in what I wrote and what you wrote, namely that I wrote left.repr <= repr instead of left.repr < repr. It's really the latter that is of interest. However, it usually comes up that you need this !in left.repr as well, in which case left.repr <= repr implies left.repr < repr. The logical encoding of left.repr < repr in Dafny is left.repr <= repr && exists x :: x !in left.repr && x in repr. That's a rather clumsy encoding, so since <= is good enough here, I suggest using left.repr <= repr && this !in repr.

I have two more comments. One is that I suggest you add a conjunct null !in repr as part of the definition of Valid(). Before I got into the habit of doing this, I several times found myself very confused about why some particular proof obligation didn't hold, only to find that it didn't hold for the value null. You can avoid such confusion by always including null !in repr (unless you have some strong reason to believe it would be convenient to allow null in repr).

The other thing is that the form of the body of your Valid() is overly complicated. After the conjunct this in repr, you have written something of the form:
(L && R) ||
((!L ==> P) && (!R ==> Q))
Note that the first disjunct (that is, L && R) is stronger than the second. Therefore, you might as well just write:
(!L ==> P) && (!R ==> Q)
Marked as answer by rustanleino on 3/18/2016 at 4:30 PM