如何修改我的帖子条件以达到 Spark 证明的黄金标准 - Ada SPARK

问题描述

我对 Ada 完全陌生，并且一直在尝试实现一些基础知识。我有一个简单的功能来抛硬币 - 不是随机的，正面应该翻转到反面，反之亦然。我添加了一个后置条件翻转（硬币）！= 硬币。应该说翻转的硬币不能等于原始硬币，但是当我尝试使用 --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;

任何帮助都会很棒！在接下来的两周内，我会提出更多要求。

解决方法

试试后置条件：

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

这确保函数结果不等于函数输入 x。

在后置条件中声明 flip(x) 确实会导致无限递归，因为每次调用 flip 都会检查后置条件。因此，该函数将始终再评估一次以检查后置条件：无限递归。