gpt4 book ai didi

computer-science - 如何修改我的发布条件以达到 Spark 证明的黄金标准 - Ada SPARK

转载 作者:行者123 更新时间:2023-12-04 13:09:31 26 4
gpt4 key购买 nike

我是 Ada 的新手,一直在尝试实现一些基础知识。我有一个简单的抛硬币功能——不是随机的,正面应该抛向反面,反之亦然。我添加了 flip(coin) != coin 的后置条件。应该说翻转的硬币一定不等于原始硬币,但是当我尝试使用 --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 周内,我会提出更多要求。

最佳答案

尝试后置条件:

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

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

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

关于computer-science - 如何修改我的发布条件以达到 Spark 证明的黄金标准 - Ada SPARK,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/67059432/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com