问题标签 [alt-ergo]

我有一组符号变量：

一组未知函数，受许多公理约束：

这里的函数f1, f2,f3是未知的，但是是固定的。所以它不是一个理论uninterpreted functions。

我想证明以下断言的有效性：

使用基于上述公理等式的替换。

对于这样的定理，是否有一种理论只会使用提供的等式来尝试组合答案，而不是对函数进行解释？

如果是这样，该理论的名称是什么，什么 SMT 求解器支持它？

它可以与其他理论混合，比如线性算术吗？

我想证明 Frama-C 中欧几里得除法的循环实现：

但是后置条件无法自动证明（循环不变量证明很好）：

它确实有欧几里得划分的所有假设，有谁知道为什么它不能得出结论？

我目前正在玩 frama-c，我正在寻找 frama-c 如何对提供给证明者（或证明助手）的各种证明义务进行编码。在这种情况下，alt-ergo。

我想知道是否有任何特定的方法可以“转储”给 alt-ergo 的输入（假设 alt-ergo 是从 frama-c 调用的；即不是互操作）？

我想看看 C 程序属性的证明义务是如何在 alt-ergo 的“本机”输入语言中编码的。任何帮助将不胜感激。

我相信我遗漏了一些明显的东西，但我已经尝试了很多，但我还没有找到问题的根源。

我正在关注 Frama-C 的 acsl指南。有这个介绍性示例说明如何验证在数组中找到最大值的正确性：

但是，运行frama-c -wp -wp-prover alt-ergo samenum.c -then -report我得到：

似乎 alt-ergo 在证明该属性之前就超时了。值得一提的是，我尝试了更高的超时时间，但它仍然不起作用。

我在用：

• 帧-c：19.1
• 为什么3：1.2.0
• alt-ergo：2.3.2

我在 Ubuntu 18.04 上运行它，在运行我运行的命令之前：why3 config --detect确保为什么 3 知道 alt-ergo。

有任何想法吗？任何人都可以验证这是示例不起作用吗？任何帮助将不胜感激！

我正在尝试使用 Frama-c 测试一个函数：

安装完所有要求后：OPAM、why3、alt-ergo 每当我执行frama-c -wp fct.c 时，我都会收到：

我试图使用 Frama-c 验证以下程序的正确性我是 frama-C 的新用户。

问题：

输入员工的基本工资，并根据以下公式计算其总工资：

基本工资 <= 10000 : HRA = 20%, DA = 80%

基本工资 <= 20000：HRA = 25%，DA = 90%

基本工资 > 20000 : HRA = 30%, DA = 95%

我在这里犯了什么错误？前提条件是否应该更精确。

控制台消息：

当我运行 WP 示例时，出现错误，我不知道它是什么。

这是 frama-c-gui 控制台中的错误

执行“frama-c -wp -wp-rte swap.c”后的输出

如果你能帮助我，非常感谢