dafny - 是否存在将不变量更改为确保子句的一种解决方案？

Question

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>,  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:=Result1;
}

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

标签： dafny