I want termination proof of divide and conquer approach to find max of array,I want equational proof in form of lemma.Below is my attempt.I have got accepted everything in dafny ,it is only pointing the termination proof as false.Below is the code-
method maxofarray(a:seq<int>) returns (max1:int)
requires |a|>=0
ensures |a|==1==>max1==a[0]|||a|>1==>maxpred(max1,a[..|a|])
decreases |a[0..|a|/2]|
{
if (|a|==1)
{
max1:=a[0];
}
else
{
var middle:=|a|/2;
var m1:=maxofarray(a[0..middle]);
var m2:=maxofarray(a[middle..|a|]);
if (m1>=m2)
{
max1:=m1;
}
else
{
max1:=m2;
}
}
}
predicate maxpred(max1:int,a:seq<int>)
{
(|a|>1)==>max1==maxfunc(a)
}
function maxfunc(a:seq<int>):int
decreases |a|
{
if |a|==1 then a[0] else
max2(
maxfunc(a[0..|a|/2]),
maxfunc(a[|a|/2..|a|])
)
}
function max2(a:int,b:int):int
requires a<b || a>b||a==b
{
if a>=b then a else b
}
I am getting the below error-
Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
C:\Users\Dell\Downloads\dafny\prog\recursion\intro\maxofarray.dfy(14,18): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
C:\Users\Dell\Downloads\dafny\prog\recursion\intro\maxofarray.dfy(35,0): Error: failure to decrease termination measure
Execution trace: