是否有一种解决方案可将不变量更改为sure子句？

问题描述

function max(a: array<int>,n:int):(int)
requires n>0
requires a.Length>n
reads a
{
   if n==1 then a[0] else 
   if max(a,n-1)<a[n] then a[n] else 
   max(a,n-1)
}

method max_one_way(a: array<int>,n: int) returns (Result:int)
   requires  n>0
   requires a.Length>n
   ensures   Result == max(a,n);
{
   var i: int;
   i := 1;
   Result := a[0];
   while (i < n)
      invariant  i <= n;
      invariant  Result == max(a,i);
   {
      i := i + 1;
      if (Result < a[i])
      {
         Result := a[i];
      }
   }
}
method max_one_way_rule1(a: array<int>,n: int,i1: int,Result1 : int) returns (Result:int,i:int)
   requires  n > 0;
   requires a.Length > n;
   requires 0< i1 < n;
   requires Result1 == max(a,i1);
   requires Result1 < a[i1+1];
   ensures i <= n; 
   ensures 0 < i < a.Length;
   ensures Result == max(a,i);
{
   i := i1+1;
   Result := a[i];
}

method max_one_way_rule2(a: array<int>,i1);
   requires Result1 > a[i1+1];
   ensures i <= n; 
   ensures 0 < i < a.Length;
   ensures Result == max(a,i);
{
   i := i1+1;
   Result:=Result1;
}

我尝试对max数组搜索进行编码，这是通过while循环进行的常规方式，例如max_one_way方法，但是我的想法是迭代调用满足条件的方法（max_one_way_rule1和rule2），对吗？提示，可以成功编译。

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）