如何编写检查数组是否已排序的dafny函数？

如何解决如何编写检查数组是否已排序的dafny函数？

我想编写一个dafny函数，与下面的谓词相同，以便可以从另一个函数（在代码中）调用它。但是，我不确定该怎么做。

predicate sorted(s: seq<char>)
{
   forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

编辑：所以我尝试了以下操作，并得到错误：stdin.dfy（8,8）：错误：在这种情况下，不允许分配给非重影变量（因为这是一个虚幻方法或因为该语句由仅用于规范的表达式保护）

关于b行：= a

method sortString(a: string) returns (b: string) 

{
    if (sorted(a)){
      b := a;
    }
}

function sorted(s: seq<char>):bool
{
   if forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j] then true else false
}

解决方法

如果您希望能够从sorted呼叫method，只需将其标记为predicate method，就像这样

predicate method sorted(s: seq<char>)
{
   forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

然后您可以像这样从method调用

method sortString(a: string) returns (b: string) 

{
    if (sorted(a)){
      b := a;
    }
}

通常，predicate只是返回function的{​​{1}}。两者之间没有区别。