问题

我试图迭代计算一个自然数序列的最大元素，但在循环不变式中出现错误。

有人能告诉我正确的代码循环不变式是什么吗？

这是代码：

```dylan
function maximo(s: seq<nat>): nat
  decreases |s|
{
  if s == [] then 0 else if s[0] > maximo(s[1..]) then s[0] else maximo(s[1..])
}

method maximo_it(s: seq<nat>) returns (max: nat) 
  ensures max == maximo(s);
{
  max := 0;
  var i := 0;

  while i < |s|
  decreases |s| - i
  invariant 0 <= i <= |s|
  invariant max == maximo(s[..i])
  { 
    if (max < s[i]) { max := s[i]; }
    i := i + 1;
  }    
}

我尝试进行了更改，但我认为我的解决方案是正确的。我看到了一种可能的解决方案，它从末尾到开头遍历序列，我的解决方案只是从零位置开始相同。

以下是解决方案的代码：

method maximo_it(s: seq<nat>) returns (max: nat) 
  ensures max == maximo(s);
{
  max := 0;
  var i := |s|;
  while i > 0
    decreases i
    invariant 0 <= i <= |s|
    invariant max == maximo(s[i..]) 
  {  
    i := i - 1; 
    if s[i] > max
    { 
      max := s[i];
    }
  }
}

<details>
<summary>英文:</summary>

I&#39;m trying to calculate the maximum element of a sequence of naturals in dafny iteratively and I get an error in the loop&#39;s invariant.

Could someone tell me which would be the correct invariant for the code?

This is the code:

function maximo (s:seq<nat>):nat
decreases |s|
{
if s == [] then 0 else if s[0] > maximo(s[1..]) then s[0] else maximo(s[1..])
}

method maximo_it (s:seq<nat>) returns (max: nat)
ensures max == maximo(s);
{
max :=0;
var i:=0;

while i < |s|
decreases |s|-i
invariant 0<=i<=|s|
invariant max == maximo(s[..i])
{

if (max < s[i]) { max:=s[i];}
i:=i+1;

}
}

I tried to change it but I do think mi solution is correct. I´ve seen a possible solution that goes across the sequence from the end to the beginning, my solution is just the same but starting from the zero position.

Here is the solution's code: 

method maximo_it (s:seq<nat>) returns (max: nat)
ensures max == maximo(s);
{

max := 0;
var i := |s|;
while i > 0
decreases i
invariant 0 <= i <= |s|
invariant max == maximo(s[i..])
{
i := i-1;
if s[i] > max
{
max := s[i];
}

}

}

</details>


# 答案1
**得分**: 2

```python
如果您想按与函数不同的顺序编写迭代代码，那么您需要一个引理来证明这两种顺序是一致的。

```python
函数 maximo(s: seq&lt;nat&gt;): nat
  减少 |s|
{
  如果 s == [] 则
    返回 0
  否则 如果 s[0] &gt; maximo(s[1..]) 则
    返回 s[0]
  否则
    返回 maximo(s[1..])
}

引理 maximo_unroll(s: seq&lt;nat&gt;)
  需要 s != []
  确保 maximo(s) == 如果 s[|s|-1] &gt; maximo(s[..|s|-1]) 则 s[|s|-1] 否则 maximo(s[..|s|-1])
{
  如果 s != [] 则 {
    变量 butlast := s[..|s|-1];
    变量 rest := s[1..];
    如果 butlast != [] 则 {
      maximo_unroll(rest);
      断言 rest[..|rest|-1] == s[1..|s|-1];
    }
  }
}

方法 maximo_it (s: seq&lt;nat&gt;) 返回 (max: nat) 
  确保 max == maximo(s);
{
  max := 0;
  变量 i := 0;

  当 i &lt; |s|
    减少 |s| - i
    不变量 0 &lt;= i &lt;= |s|
    不变量 max == maximo(s[..i])
  { 
    maximo_unroll(s[..i+1]);
    断言 s[..i+1][..|s[..i+1]|-1] == s[..i];

    如果 (max &lt; s[i]) 则 {
      max := s[i];
    } 
    i := i+1;
  }
  断言 s == s[..|s|];
} 

function maximo(s: seq<nat>): nat
  decreases |s|
{
  if s == [] then
    0
  else if s[0] > maximo(s[1..]) then
    s[0]
  else
    maximo(s[1..])
}

lemma maximo_unroll(s: seq<nat>)
  requires s != []
  ensures maximo(s) == if s[|s|-1] > maximo(s[..|s|-1]) then s[|s|-1] else maximo(s[..|s|-1])
{
  if s != [] {
    var butlast := s[..|s|-1];
    var rest := s[1..];
    if butlast != [] {
      maximo_unroll(rest);
      assert rest[..|rest|-1] == s[1..|s|-1];
    }
  }
}

method maximo_it (s: seq<nat>) returns (max: nat) 
  ensures max == maximo(s);
{
  max := 0;
  var i := 0;

  while i < |s|
    decreases |s| - i
    invariant 0 <= i <= |s|
    invariant max == maximo(s[..i])
  { 
    maximo_unroll(s[..i+1]);
    assert s[..i+1][..|s[..i+1]|-1] == s[..i];

    if (max < s[i]) {
      max := s[i];
    } 
    i := i+1;
  }
  assert s == s[..|s|];
} 

答案2

得分: 2

与其使用词形，这种情况下的另一个选择是调整 `maximo()` 函数本身。这是我想出的最干净的解决方案：

```lang-dafny
function maximo(s:seq<nat>, n: nat):(r:nat)
requires n <= |s|
decreases n
{
    if n == 0 then 0
    else
        var last := s[n-1];
        var max := maximo(s,n-1);
        if last >= max then last
        else max
}

method maximo_it(s:seq<nat>) returns (max: nat)
ensures max == maximo(s,|s|);
{
  max :=0;
  var i:=0;

  while i < |s|
  decreases |s|-i
  invariant i <= |s|
  invariant max == maximo(s,i)
  {
    if max <= s[i] { max := s[i]; }
    i:=i+1;
  }
}

在这里，我重新调整了 maximo() 函数的迭代顺序。

<details>
<summary>英文:</summary>

Instead of using a lemma, another option in this case is to tweak the `maximo()` function itself.  This is the cleanest solution I came up with:

```lang-dafny
function maximo(s:seq&lt;nat&gt;, n: nat):(r:nat)
requires n &lt;= |s|
decreases n
{
    if n == 0 then 0
    else
        var last := s[n-1];
        var max := maximo(s,n-1);
        if last &gt;= max then last
        else max
}

method maximo_it(s:seq&lt;nat&gt;) returns (max: nat)
ensures max == maximo(s,|s|);
{
  max :=0;
  var i:=0;

  while i &lt; |s|
  decreases |s|-i
  invariant i &lt;= |s|
  invariant max == maximo(s,i)
  {
    if max &lt;= s[i] { max := s[i]; }
    i:=i+1;
  }
}

Here, I've reworked the order of iteration for the maximo() function.