ACSL中的PreCondition或PostCondtion

Question

在ACSL中，我无法区分各种先决条件和后条件.正如我所知道的那样，终止和承担是在前提条件下进行的，并且保证和分配在后状态。但在哪一种安息如减少等是？？

有人能帮我弄清楚吗？提前感谢

Answer 1

这是刁钻的问题。基本上，decreases可以作为递归调用的一个先决条件:如果您有一个带有decreases x;的函数f，如果它碰巧调用了它自己，那么您必须证明这个调用站点上的x<\at(x,Pre)。此外，当您调用x>=0 (递归调用与否)时，您有一个前置条件，即f。关于其他从句(根据其在ACSL 1.7中的顺序)

• complete和disjoint子句基本上是契约的assumes子句的逻辑属性，它们并不意味着任何用于实现的内容，而是作为规范本身的健全检查。
• allocates和frees是后置条件(与assigns类似，但涉及动态分配)。
• exits (以及returns、breaks和continues)是后置条件(当我们退出函数-or语句时对它们进行评估)。
• 依赖项(\from)是后置条件(如assigns)。

Answer 2

ACSL的减子句主要用于递归函数调用。如果您指定了带有指针变量x的减值子句，例如:减*x；那么它的意思是，每当控件输入与此减额子句相关的函数时，它都会检查指针x所指向的值是否比函数预状态期间x所指向的值少1。第一次调用该函数时，预条件检查是：(*x) >= 0，因为该函数处于预状态，因此没有预状态值可与之比较。