frama-c - ACSL 中的前置条件或后置条件

Question

我无法区分 ACSL 中的各种前置条件和后置条件。据我所知，要求、终止和假设出现在前置条件中，并在后置条件中确保和分配。但在哪一组休息，如减少等？

任何机构都可以帮助我弄清楚吗？提前致谢

Answer 1

这是一个技巧问题。基本上，decreases将作为递归调用的先决条件：如果你有一个f带有的函数decreases x;，如果它碰巧调用了自己，你必须x<\at(x,Pre)在这个调用站点证明这一点。此外，您有一个先决条件，即x>=0当您调用时f（递归调用与否）。关于其他条款（基于它们在ACSL 1.7中的出现顺序：

• complete和disjoint条款基本上是assumes合同条款的逻辑属性，它们并不意味着任何实现，而是作为规范本身的健全性检查。
• allocates并且frees是后置条件（类似于assigns但关于动态分配）
• exits(and returns, breaksand continues) 是后置条件（它们在我们退出函数或语句时被评估）。
• 依赖项（\from）是后置条件（如assigns）。

Answer 2

ACSL 的减少子句基本上用于递归函数调用。如果您使用指针变量 x 指定了减少子句，例如：减少 *x; 那么它的意思是，每次控制进入与这个减少子句相关的函数时，它都会检查指针x指向的值是否比函数前状态期间x指向的值小1 . 第一次调用函数时，检查的前置条件是： (*x) >= 0，因为函数处于其前置状态，因此没有前置状态值可比较。