Dafny - function post-conditions break termination checking

Nov 15, 2012 at 1:56 PM
Edited Nov 15, 2012 at 1:57 PM

I have noticed that sometimes, if I add a property about a function as a post-condition of the function itself, it stops termination checking from succeeding. Whereas if I separate the property out as a ghost method then everything works fine. I have some hunch on the reason for this, but cannot quite put my finger on it.

I have several examples where this is the case, but these are the simplest I've found:

Base definitions and ghost methods - termination and property checking succeeds:

datatype natr = zero | suc(natr);

function add(x : natr, y : natr) : natr
{
  match x
  case zero => y
  case suc(x') => suc(add(x', y))
}

ghost method prop_add_zero_A()
  ensures forall x :: add(x, zero) == x;
{ }

ghost method prop_add_zero(x : natr)
  ensures add(x, zero) == x;
{ }

Give a post-conditon for "add", termination checking fails:

function add(x : natr, y : natr) : natr
  ensures add(x, zero) == x;
{ ... }

Locally scoping "x", termination checking fails:

function add(x : natr, y : natr) : natr
  ensures forall x :: add(x, zero) == x;
{ ... }

Setting the value of "y" with an antecedent, termination checking succeeds:

function add(x : natr, y : natr) : natr
  ensures y == zero ==> add(x, y) == x;
{ ... }

Setting the value of "y" with an antecedent, and locally scoping the variables, termination checking fails:

function add(x : natr, y : natr) : natr
  ensures forall x, y :: y == zero ==> add(x, y) == x;
{ ... }