我想找到一些可以应用于函数或函数指针的 ACSL 注释，以表明它具有引用透明的属性。以某种方式说“当给定相同的参数时，此函数将始终返回相同的值”。到目前为止，我还没有找到任何这样的方法。谁能给我指出一种表达方式？
也许某种方式来引用任意逻辑函数？如果我可以命名一个未知数logic boolean uknown_function(void* a, void* b) = /* this is unkown */;，那么我可以将一个函数记录为具有\result等于这个任意/未知逻辑函数的后置条件？
更大的上下文是尝试进行类型擦除比较。我想概括地表达“用户给了我void*s 和 abool (*)(void const*, void const*)来比较它们的概念，并且用户向我保证，所提供的函数确实是严格的偏序，无论这些指针指向什么。” 如果我有这个，那么我可以开始描述这些被排序的类型擦除对象的属性，例如。
在 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 函数的多个调用相关的属性的方法。它在此处和此处进行了描述，公开发布应该在不久的将来发生。