Mar 10, 2015 at 4:25 PM
Edited Mar 10, 2015 at 4:47 PM

I'm trying to use Dafny for proving correctness of program transformations of general schemas.
The first problem is that a function f like
type T
type T'
predicate a (x:T)
function h (x:T): T'
function c (x:T,a1:T',a2:T'): T'
function t1 (x:T): T
function t2 (x:T): T
function f (x:T): T'
{
if a(x) then h(x) else c(x,f(t1(x)),f(t2(x)))
}
cannot be proved to terminate, in fact termination of f depends on t1 and t2 which are undefined (abstract) functions.
Could someone tell me how to avoid this problem?

