Dafny: termination with datatypes problem

Mar 25, 2012 at 6:51 PM

I'm wonder why Dafny can't prove termination in this program http://rise4fun.com/Dafny/TScE . As I understand this program should be correct because function hasDegree is invoked with ValidP(rem), i.e. with its correct precondition. I add decreases clause (decreases size(poly)) but it doesn't solve the problem.

Coordinator
Apr 5, 2012 at 3:09 AM

In your program, ValidP and hasDegree are mutually recursive functions.  To prove their termination, one needs to supply a "decreases" clause that for each recursive call evaluates to a strictly smaller value.  What works for this program is:

function hasDegree(degree : nat, poly: Polynom) : bool
  decreases poly, true;
  ...
 

 

 functionValidP(poly : Polynom) : bool
 
decreases poly, false;
  ...

This works because:  For the call from hasDegree(degree,poly) to ValidP(poly), the decreases clause (which is a lexicographic tuple) goes from (poly,true) to (poly,false), which is strictly smaller.  And for the call from ValidP(poly) to hasDegree(...,rem), the decreases clause goes from (poly,false) to (rem, true), which is smaller because "rem" is a component of "poly".

I chose "false" and "true", but you could also have used "17" and "280", or "{25,1024}" and "{25,1024,-degree}", as long as the former is strictly smaller than the latter.

Note that you can use a datatype value itself (here of type Polynom) in the datatype.  That is, you don't need to compute a "size" integer for it and then use that integer in the decreases clause.  (But in this case, you also need a second part of the lexicographic tuple, in order to have the decreases clause go down in the hasDegree->ValidP call.)

If no decreases clause is provided, Dafny will make a guess, namely the lexicographic tuple consisting of the function's arguments.  (Well, more or less.  It excludes arguments whose type is a type parameter.)  But that's not quite good enough in this program, so you have to write your own decreases clauses.

Finally, any decreases clause is implicitly padded with "top" elements, which are strictly larger than any other value.  Therefore, you can actually use just "decreases poly;" for hasDegree, since this really means "decreases poly, top, top, top, top, ...", and this will make sure that the call to ValidP decreases the tuple (which is really "decreases poly, false, top, top, top, ...").  But you may find that "poly,true" and "poly,false" look easier to understand than "poly" and "poly,false".

The final program is:  http://rise4fun.com/Dafny/a0hY

Apr 11, 2012 at 3:42 PM

Thank you, Rustan!