Блог

Я хочу написать функцию 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 из a method , просто пометьте его как a 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;
    }
}
  

Кроме того, в общем случае a predicate — это просто a function , который возвращает bool . Между ними нет разницы.