确保证明代码有缺陷？

在下面，当相关的C代码被注释掉时，行为neg_limit的后置条件如何被证明是真实的？确保证明代码有缺陷？

安全 - >检查算术溢出之一是不可证明的，如预期的，但它似乎像neg_limit也应该是无法证明的。

语境：我使用的邮资-C-硼，杰西，并通过gWhy，按住Alt键人体工程学，以学习如何编写规范和证明功能的满足他们。任何关于规范策略，工具等的提示，RTFMing等也是值得赞赏的。到目前为止，我正在阅读ACSL 1.7实施手册（这是更近期的-Boron's）和Jessie教程& ref。手册。

谢谢！

/*@ behavior non_neg: 
     assumes v >= 0; 
     ensures \result == v; 

    behavior neg_in_range: 
     assumes INT32_MIN < v < 0; 
     ensures \result == -v; 

    behavior neg_limit: 
     assumes v == INT32_MIN; 
     ensures \result == INT32_MAX; 

    disjoint behaviors; 
    complete behaviors; 
*/ 
int32_t my_abs32(int32_t v) 
{ 
    if (v >= 0) 
    return v; 

    //if (v == INT32_MIN) 
    // return INT32_MAX; 

    return -v; 
}

这是第一个后置条件的gWhy目标：

goal my_abs32_ensures_neg_limit_po_1: 
    forall v_2:int32. 
    (integer_of_int32(v_2) = ((-2147483647) - 1)) -> 
    (integer_of_int32(v_2) >= 0) -> 
    forall __retres:int32. 
    (__retres = v_2) -> 
    forall return:int32. 
    (return = __retres) -> 
    ("JC_13": (integer_of_int32(return) = 2147483647))

和第二：

goal my_abs32_ensures_neg_limit_po_2: 
    forall v_2:int32. 
    (integer_of_int32(v_2) = ((-2147483647) - 1)) -> 
    (integer_of_int32(v_2) < 0) -> 
    forall result:int32. 
    (integer_of_int32(result) = (-integer_of_int32(v_2))) -> 
    forall __retres:int32. 
    (__retres = result) -> 
    forall return:int32. 
    (return = __retres) -> 
    ("JC_13": (integer_of_int32(return) = 2147483647))

来源

2013-07-30 Barrie Slaymaker

是的，这个昵称为“硼”的版本相当古老。它是http://frama-c.com/上可用的Windows二进制文件的最新版本。这可能是你使用它的原因。您是否尝试过StéphaneDuprat（http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2012-February/003040.html）编写的说明以获得两个版本？ –

@ pascal-cuoq，我现在要做，谢谢，现在正在与WP合作。如果其他人发现这一点，alt-ergo-0.94-mingw.exe似乎是必需的。 Niton-over-Boron指令指出它，但似乎并不需要它。要安装：下载它，重命名为alt-ergo.exe，然后将它放在你的PATH之前的Boron仓中。我避免使用alt-ergo-0.95-mingw.exe，因为它的网站表示它与Frama-C-Oxygen不兼容，已知0.94与Nrogen一起使用。另外：按照该链接的说明设置全部三个FRAMAC_ * env。瓦尔; INSTALL.txt只提到一个。谢谢！ –

关于文件，你可能想在弗劳恩霍夫发展论坛看看” ACSL By Example：http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf

关于你的问题，我用Frama-C Fluorine重复了你的结果（顺便说一句，你在代码中缺少#include <stdint.h>"），而Jessie + Alt-ergo仍然设法证明后置条件。但请记住，假设没有发生运行时错误（这不是代码的情况），因为失败的安全PO显示后条件被证明为。

即，第二个后置条件包含假设(integer_of_int32(result) = (-integer_of_int32(v_2)))，其可以被重写为(integer_of_int32(result) = 2147483648)。这与杰西的前奏中的一条公理相矛盾，那就是那个 forall v:int32. integer_of_int32(v)<=2147483647。

我想这再一次概括说明，只要某些证明义务没有被检查，即使它们不直接源自此注释，您也不能声称验证了ACSL注释。

来源

2013-07-31 09:34:20 Virgile

谢谢 - 非常丰富！这个（矛盾的）假设如何让alt-ergo证明integer_of_32（return）== 2147483647？例如，这样的矛盾是否允许alt-ergo证明所有的假设，或者是由于所有结果而找到一个证明：int32（例如）只能覆盖int32？gWhy中的证明步骤（对不起 - gWhy不会让我复制到剪贴板）通过你提到的假设（H8，在这里），然后通过__retres并返回假设。 –

这不仅仅是alt-ergo。基本上，只要你有两个相互矛盾的假设，你可以证明任何事情。这是一个非常古老的逻辑规则，实际上它有一个拉丁名字：_Ex falso quod libet_（来自false [演绎]你想要的）。 – Virgile

我们如何知道有一整套安全PO（WP中的RTE POs，现在我使用Flourine）生成，因此至少有一个在这种情况下总会失败，其中Frama生成的矛盾假设-C启用假证明？我认为，防止Frama-C从非矛盾的规范PO中产生矛盾的假设是不可能的，或者至少是不可行的。 –

确保证明代码有缺陷？

回答

相关问题