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

I have noticed that sometimes, if I add a property about a function as a postcondition 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 postconditon 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;
{ ... }
