在ACSL中指定引用透明度

Question

我希望找到一些可以应用于函数或函数指针的ACSL注释，以表明它具有引用透明性。某种说法是“当给定相同的参数时，此函数将始终返回相同的值”。到目前为止我还没有找到这样的方法。有人能告诉我怎么表达吗？

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

更大的背景是尝试进行类型擦除比较。我通常想表达这样的概念：“用户给了我一个void*和一个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函数的几个调用相关的属性。它被描述为这里和这里，在不远的将来应该会公开发布。