как написать функцию 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
}

dafny
person george    schedule 09.11.2020    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Если вы хотите иметь возможность вызывать 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, возвращающее bool. Между ними нет никакой разницы.

person James Wilcox    schedule 10.11.2020