在 ACSL 中指定参照透明性
Specifying Referential transparency in ACSL
我想找到一些可以应用于函数或函数指针的 ACSL 注释，以指示它具有引用透明性的 属性。某种方式说 "this function will always return the same value when given the same arguments"。到目前为止，我还没有找到任何这样的方式。谁能告诉我一种表达方式？
也许可以通过某种方式来引用任意逻辑函数？如果我可以命名一个未知的 logic boolean uknown_function(void* a, void* b) = /* this is unkown */; 那么我可以将一个函数记录为具有后置条件它 \result 等于这个 arbitrary/unknown 逻辑函数？
更大的上下文正在尝试进行类型擦除比较。我想概括地表达 "the user has given me void*s to work with and a bool (*)(void const*, void const*) to compare them with, and the user is guaranteeing to me that the function provided really is a strict partial order over whatever those pointers point to." 的概念 如果我有这个概念，那么我就可以开始描述正在排序的这些类型擦除对象的属性，例如。
在 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 and here，public 版本应该在不久的将来发生。
我想找到一些可以应用于函数或函数指针的 ACSL 注释，以指示它具有引用透明性的 属性。某种方式说 "this function will always return the same value when given the same arguments"。到目前为止，我还没有找到任何这样的方式。谁能告诉我一种表达方式？
也许可以通过某种方式来引用任意逻辑函数？如果我可以命名一个未知的 logic boolean uknown_function(void* a, void* b) = /* this is unkown */; 那么我可以将一个函数记录为具有后置条件它 \result 等于这个 arbitrary/unknown 逻辑函数？
更大的上下文正在尝试进行类型擦除比较。我想概括地表达 "the user has given me void*s to work with and a bool (*)(void const*, void const*) to compare them with, and the user is guaranteeing to me that the function provided really is a strict partial order over whatever those pointers point to." 的概念 如果我有这个概念，那么我就可以开始描述正在排序的这些类型擦除对象的属性，例如。
在 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 and here，public 版本应该在不久的将来发生。