Как изменить условие публикации для достижения золотого стандарта Spark proof — Ада СПАРК

Я совершенно новичок в Аде и пытаюсь реализовать некоторые основы. У меня есть простая функция подбрасывания монеты - не случайным образом, решка должна переворачиваться орлом и наоборот. Я добавил условие публикации, что флип (монета) != монета. Предполагается, что перевернутая монета не должна равняться исходной монете, но когда я пытаюсь проверить файл с --mode gold, я получаю следующие предупреждения:

flip_coin.ads:8:06: warning: postcondition does not mention function result
flip_coin.ads:8:14: warning: call to "flip" within its postcondition will lead to infinite recursion
flip_coin.ads:8:14: medium: postcondition might fail, cannot prove flip(x) /= x[#0]

Вот рекламный файл

package flip_coin with SPARK_Mode
is
  type Coin is (Heads, Tails);

  function flip (x : Coin) return Coin with
   Post => flip(x) /= x;
end flip_coin;

А вот файл .adb

package body flip_coin with SPARK_Mode
is

  function flip (x : Coin) return Coin
  is
  begin
    if x = Heads then return Tails; else return Heads; end if;
  end flip;

end flip_coin;

Любая помощь будет здорово! Я буду спрашивать много больше в течение следующих 2 недель.


computer-science ada formal-methods spark-ada
person Lee Robinson    schedule 12.04.2021    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Попробуйте постусловие:

function flip (x : Coin) return Coin with
   Post => flip'Result /= x;

Это гарантирует, что результат функции не равен входу функции x.

Указание flip(x) в вашем постусловии действительно приведет к бесконечной рекурсии, поскольку постусловие будет проверяться при каждом вызове flip. В результате функция всегда будет оцениваться еще раз, чтобы проверить постусловие: бесконечная рекурсия.

person DeeDee    schedule 12.04.2021
comment
Идеально Спасибо! Я попробовал flip'Result(x) /= x, что не сработало, и теперь я знаю, почему. удивительно! - person Lee Robinson; 12.04.2021