Указание ссылочной прозрачности в ACSL
Я хочу найти некоторую аннотацию ACSL, которую можно применить к функции или указателю на функцию, чтобы указать, что она обладает свойством ссылочной прозрачности. Некоторый способ сказать, что "эта функция всегда будет возвращать одно и то же значение, если даны одинаковые аргументы" До сих пор я не нашел такой способ. Может кто-нибудь указать мне способ выразить это?
Может быть, какой-нибудь способ сослаться на произвольную логическую функцию? Если бы я мог назвать неизвестное logic boolean uknown_function(void* a, void* b) = /* this is unkown */; тогда я мог бы задокументировать функцию с постусловием, что это \result равно этой произвольной / неизвестной логической функции?
Более широкий контекст пытается сделать сравнение типа стертых. Я хочу в целом выразить концепцию "пользователь дал мне void*с работать и bool (*)(void const*, void const*) чтобы сравнить их с, и пользователь гарантирует мне, что предоставленная функция действительно является строгим частичным порядком по отношению к тому, на что указывают эти указатели."Если бы у меня было это, то я мог бы начать описывать свойства сортируемых типов стертых объектов, например.
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. Это описано здесь и здесь, и публичное издание должно произойти в недалеком будущем.