0
$\begingroup$

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:
$\endgroup$
2
  • $\begingroup$ We are not a coding site. I don't think asking us to provide proofs of correctness for a bunch of code is on-topic here. Any community votes? (We're looking to build up an archive of knowledge that will be useful to others in the future. It seems hard to see how this question will be useful to anyone else unless they are trying to do exactly the same thing with exactly the same code.) $\endgroup$
    – D.W.
    Mar 8, 2022 at 21:19
  • $\begingroup$ Please proof-read your post. The lack of indentation makes your code hard to read. You received a similar comment on your last post, too. $\endgroup$
    – D.W.
    Mar 8, 2022 at 21:19

1 Answer 1

1
$\begingroup$

The problem got solved ,below is the fully verified code.

method maxofarray(a:seq<int>) returns (max1:int)
requires (|a|==1)|| (|a|>=2 && |a|>1  )
ensures (|a|==1==>max1==a[0])||(|a|>1==>|a|>=2 ==>maxpred(max1,a[..|a|]))
decreases |a|/2 
{
if (|a|==1)
{
max1:=a[0];

}
else
{
var m1:=maxofarray(a[0..|a|/2]);
var m2:=maxofarray(a[|a|/2..(|a|/2+|a|/2)]);
if (m1>=m2)
{
max1:=m1;
}
else
{
max1:=m2;
}
}
}
predicate maxpred(max1:int,a:seq<int>)
{
|a|>1 ==> |a|>=2==>max1==maxfunc(a)
}
function maxfunc(a:seq<int>):int
requires (|a|==1)|| (|a|>=2  )
decreases |a|/2 
{

if |a|==1 then a[0] else
 max2(
maxfunc(a[0..|a|/2]),
maxfunc(a[|a|/2..(|a|/2+|a|/2)])
)
}
function max2(a:int,b:int):int
requires a<b || a>b||a==b

{
if a>=b then a else b
}
method maxofarray(a:seq<int>) returns (max1:int)
requires (|a|==1)|| (|a|>=2 && |a|>1  )
ensures (|a|==1==>max1==a[0])||(|a|>1==>|a|>=2 ==>maxpred(max1,a[..|a|]))
decreases |a|/2 
{
if (|a|==1)
{
max1:=a[0];

}
else
{
var m1:=maxofarray(a[0..|a|/2]);
var m2:=maxofarray(a[|a|/2..(|a|/2+|a|/2)]);
if (m1>=m2)
{
max1:=m1;
}
else
{
max1:=m2;
}
}
}
predicate maxpred(max1:int,a:seq<int>)
{
|a|>1 ==> |a|>=2==>max1==maxfunc(a)
}
function maxfunc(a:seq<int>):int
requires (|a|==1)|| (|a|>=2  )
decreases |a|/2 
{

if |a|==1 then a[0] else
 max2(
maxfunc(a[0..|a|/2]),
maxfunc(a[|a|/2..(|a|/2+|a|/2)])
)
}
function max2(a:int,b:int):int
requires a<b || a>b||a==b

{
if a>=b then a else b
}
Dafny program verifier finished with 4 verified, 0 errors
Compiled assembly into maxofarray.dll
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.