在 ACSL 中指定参照透明度

Question

我想找一些可以应用于函数或函数指针的ACSL注解来表明它具有引用透明的属性。以某种方式说“当给定相同的参数时，此函数将始终返回相同的值”。到目前为止，我还没有找到任何这样的方法。谁能给我指出一种表达方式？

也许可以通过某种方式引用任意逻辑函数？如果我可以命名一个未知的logic boolean uknown_function(void* a, void* b) = /* this is unkown */;，那么我可以将一个函数记录为具有\result 的后置条件等于这个任意/未知的逻辑函数？

更大的上下文是尝试进行类型擦除比较。我想概括地表达“用户给了我void*s 和bool (*)(void const*, void const*) 来比较它们的概念，并且用户向我保证所提供的功能确实是一个严格的偏序。那些指针指向。”如果我有这个，那么我就可以开始描述这些被排序的类型擦除对象的属性，例如。

Answer 1

在 ACSL 中确实没有直接的可能性：函数合约仅指定在函数的单次调用期间会发生什么。您确实可以依赖已声明但未定义的逻辑函数，使用 reads 子句指定该函数需要计算其结果的 C 内存状态部分，例如

/*@ logic boolean unknown_function{L}(int* a, int* b) reads a[0 .. 1], b[2 .. 3]; */

但是如果你使用void *，在不知道底层对象大小的情况下，这可能很难指定：除非unknown_function 的结果仅依赖于指针的值，而不是指针的内容指向对象，在这种情况下，您不需要 reads 技巧。

另外请注意，尚不支持基于函数指针的合同，如果我正确理解您的最后一段，这可能是您打算做什么的问题。

最后，您可能对即将推出的插件 RPP 感兴趣，它提出了一种指定、证明和使用与一个或多个 C 函数的多次调用相关的属性的方法。它被描述为here 和here，并且应该在不久的将来公开发布。